Groups | Search | Server Info | Login | Register

Groups > sci.logic > #254139

Re: Expressability in the notation of set theory

Show all headers | View raw

Doing such meta-mathematics has different 
routes. One route uses what Gödel paved, you can
do many theorems by using some Gödelization.

A Gödel numbering can be interpreted as an encoding 
in which a number is assigned to each symbol of a 
mathematical notation, after which a sequence of 
natural numbers can then represent a sequence of symbols.
https://en.wikipedia.org/wiki/G%C3%B6del_numbering

This means you use natural numbers to encode
formulas, programs, what ever ..., which works when
the formulas, programs, what ever ..., are countably

many. You might also work with infinite axiom sets,
generated by axiom schemas, if they are countably many,
and all this is recursively enumerable.

Today you can do meta-mathematics in Coq, Isabelle/HOL,
etc.. by means of lambda calculus. You don't need to go
the pain road of encoding in natural numbers, some stuff can

be done via so called HOAS approaches.

In computer science, higher-order abstract syntax 
(abbreviated HOAS) is a technique for the representation 
of abstract syntax trees for languages with variable binders.
https://en.wikipedia.org/wiki/Higher-order_abstract_syntax

Have Fun!

Mild Shock schrieb am Freitag, 9. Juni 2023 um 09:28:14 UTC+2:
> This is all related to recursion theory. You will go into 
> domain where Olcott is constantly fabulating. I never 
> saw you react to Olcotts nonsense. 
> 
> I also never saw you producing some results with 
> DC Proof that relate to recursion theory, except a 
> little little Peano arithmetic, one time 
> 
> you prove the existence of add. But mostlikely you 
> don't know whether add is primitive recursive or not. 
> Concerning first Non-First-Order-isability, you might 
> 
> also go into the waters of the Halting Problem: 
> 
> "If the machine M does halt in finite steps, then the complete computation 
> record is also finite, then there is a finite initial segment of the natural 
> numbers such that the arithmetical sentence \phi _{M} is also true on this 
> initial segment. Intuitively, this is because in this case, proving 
> \phi _{M} requires the arithmetic properties of only finitely many numbers." 
> https://en.wikipedia.org/wiki/Trakhtenbrot%27s_theorem#Intuitive_proof
> Mild Shock schrieb am Freitag, 9. Juni 2023 um 09:21:29 UTC+2: 
> > Whats your goal? Even if you can formalize the 
> > statement itself. The results around the statement possibly 
> > involved some model theory etc.. in the old times this 
> > 
> > was called meta-mathematics. What is your plan? The blog by 
> > Terrence Tao itself is not very helpful, since he writes "I can’t 
> > quite show that (*) is not expressible in first-order logic" 
> > So you need to look elsewhere for hints whats going on. 
> > Dan Christensen schrieb am Freitag, 9. Juni 2023 um 06:19:38 UTC+2: 
> > > (Correction) 
> > > 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 r1]] 
> > > & ALL(a):[a in u => EXIST(b):[b in u & (a,b) in r21]] 
> > > 
> > > & ALL(x):ALL(x'):ALL(y):ALL(y'):[x in u & x' in u & y in u & y' in u => [(x,y) in r1 & (x',y') in r2 => Q(x,x',y,y')]] 
> > > 
> > > 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