Groups | Search | Server Info | Login | Register

Groups > sci.logic > #254091

Re: Expressability in the notation of set theory

Show all headers | View raw

To show that the FOL result, and also the SOL original,
is special, you need to follow an application of
the branching quantifier, namely that it can express:

It is also powerful enough to define the quantifier "there are infinitely many"
Several things follow from this, including the nonaxiomatizability of first-
order logic with (first observed by Ehrenfeucht), and its equivalence to the 
\Sigma _{1}^{1}-fragment of second-order logic (existential 
second-order logic)—the latter result published independently in 1970 by 
Herbert Enderton and W. Walkoe.
https://en.wikipedia.org/wiki/Branching_quantifier

It says two things:
a) The problem of having complete ruleset for 
  general validity in second order logic, something similar
  like application of Trakhtenbrot's theorem to show second
  order logic has no calculus
https://en.wikipedia.org/wiki/Trakhtenbrot%27s_theorem

b) That a calculus is already missing for the
  existential second order logic sublanguage. So this
  fragment makes it already hard to find a calculus!

And we might want to know two other things:
c) It would also show that DC Poop, which has function 
  quantifiers, is not complete. So despite all the fun
  of translation second order logic to first order logic,
  the limitations of such translations are the limitations
  that Terrence Tao mentioned Non-Firstorderisability,
  in the sense that a second order sentence can ideally
  express something, that a first order sentence isn't able
  to "faithfully" reflect.

d) But the outlook isn't that grim at all, if we 
  abandon the ideal of second order logic, and
  go with some general models via some
  Henkin semantics, we might nevertheless find
  calculi. An intersting article about that by Enderton:

Second-order and Higher-order Logic
First published Thu 20 Dec, 2007 - Herbert B. Enderton
https://plato.stanford.edu/archives/win2007/entries/logic-higher-order/

Funny coincidence the SEP article has a section "Syntax 
and translation". But his translation is not the one I have in mind.
Come on, its not that difficult. Its rather straight forwared.

Mild Shock schrieb am Donnerstag, 8. Juni 2023 um 10:03:16 UTC+2:
> The Problem is Terrence Tao wrote: 
> "I can’t quite show that (*) is 
> not expressible in first-order logic" 
> 
> And you find only some nuggets dealing more with 
> the problem in the comment section. The sentence 
> in question is then this second order logic sentence, 
> 
> when skolemize it: 
> 
> /* Terrence Taos Example Skolemized */ 
> ∃f∃g∀x∀yQ(x,y,f(x),g(y)) 
> https://en.wikipedia.org/wiki/Branching_quantifier 
> 
> But then you have again an instance of the Problem, 
> how translate second order logic to first order logic. 
> Which you seem not aware how to do it. Certainly 
> 
> you don't need to touch Q, unless you want also 
> express ∀Q or something, since Q is first order, its 
> arguments x, y, f(x), g(y) are all individuals, so 
> 
> Q is a first order predicate. Nothing to change for 
> Q. The only thing that is not first order, are the two 
> quantifiers ∃f and ∃g. 
> 
> So how do you translate second order 
> to first order, any clue?
> Mild Shock schrieb am Donnerstag, 8. Juni 2023 um 09:51:45 UTC+2: 
> > Maybe lets first try something simpler. A translation from second 
> > order logic to first order logic of this example: 
> > 
> > /* Drinker Paradox */ 
> > ∀D∃x(Dx → ∀yDy) 
> > 
> > The idea is that the translation is neither a generalization nor 
> > a specialization, but "faithful". 
> > 
> > Can you do it Danny Boy? 
> > Dan Christensen schrieb am Donnerstag, 8. Juni 2023 um 05:25:40 UTC+2: 
> > > The following from Terence Tao's blog dated 2007-08-27: 
> > > 
> > > "It seems that one cannot express 
> > > 
> > > "'For every x and x’, there exists a y depending only on x and a y’ depending only on x’ such that Q(x,x’,y,y’) is true' 
> > > 
> > > "in first order logic!" 
> > > 
> > > https://terrytao.wordpress.com/2007/08/27/printer-friendly-css-and-nonfirstorderizability/#more-172 
> > > 
> > > Following is my attempt to formalize this statement using the notation of set theory in DC Proof: 
> > > 
> > > ALL(a):[a in u => EXIST(b):[b in u & (a,b) in r]] 
> > > 
> > > & ALL(x):ALL(y):[x in u & y in u => ALL(a):ALL(b):ALL(c):ALL(d):[(a,b,c,d) in q 
> > > <=> (a,b,c,d) in u4 & [a=x & b=y & (x,c) in r & (y,d) in r]]] 
> > > 
> > > where u4 = u*u*u*u (Cartesian product) 
> > > 
> > > Comments? 
> > > 
> > > Dan 
> > > 
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com 
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

Back to sci.logic | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-07 20:25 -0700
  Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-07 22:11 -0700
    Re: Expressability in the notation of set theory Julio Di Egidio <julio@diegidio.name> - 2023-06-07 23:34 -0700
      Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 07:31 -0700
  Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 00:51 -0700
    Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 01:03 -0700
      Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 01:19 -0700
      Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 08:04 -0700
        Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 11:10 -0700
          Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 11:40 -0700
          Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 11:51 -0700
            Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 12:16 -0700
              Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 12:34 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 13:47 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 13:57 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 14:11 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 14:42 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 14:45 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 14:51 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 14:57 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 15:04 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 15:09 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 15:28 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 15:48 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-08 15:54 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 19:43 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 19:32 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 14:38 -0700
  Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-08 21:19 -0700
    Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-09 00:21 -0700
      Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-09 00:28 -0700
        Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-09 00:34 -0700
          Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-09 00:48 -0700
      Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-09 06:57 -0700
        Re: Expressability in the notation of set theory Mild Shock <janburse@fastmail.fm> - 2023-06-09 21:04 +0200
          Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-09 13:28 -0700
            Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-09 15:42 -0700
              Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-09 15:58 -0700
                Re: Expressability in the notation of set theory Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-06-10 13:36 -0700
              Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-09 18:17 -0700
              Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-09 18:20 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-10 04:30 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-10 04:46 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-10 10:52 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-10 11:06 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-10 11:11 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-10 11:17 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-12 00:37 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-12 00:38 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-12 07:22 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-12 08:17 -0700
                Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-10 11:21 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-10 11:27 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-10 15:10 -0700
                Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-11 02:02 -0700
    Re: Expressability in the notation of set theory Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-06-09 12:03 -0700
      Re: Expressability in the notation of set theory Mild Shock <janburse@fastmail.fm> - 2023-06-09 21:12 +0200
        Re: Expressability in the notation of set theory Mild Shock <janburse@fastmail.fm> - 2023-06-09 21:22 +0200
          Re: Expressability in the notation of set theory Mild Shock <bursejan@gmail.com> - 2023-06-09 12:33 -0700

csiph-web