[FOM] Embedding intuitionistic logic in classical

[GMAIL]

>The disclaimer here is, of course, that the result doesn't guarantee 

>computability of the translation for predicate logics. I wonder if it could
be extended?

 

Staffan

 

We just happen to have recursively translated (embedded) predicate logic
into a propositional logic which is very close to classical propositional
logic. Here is a short description of our result, it improves Tarski's
result in the Tarski-Givant book "Formalizing set theory without variables".

 

Announcement of new result and preprint

 

We proved that first-order logic can be recursively translated into a very
simple and weak logic, and thus set theory can be formalized in this weak
logic. This weak logical system is equivalent to the equational theory of
Boolean algebras with three commuting complemented closure operators, i.e.,
diagonal-free 3-dimensional cylindric algebras Df3. Equivalently, set theory
can be formulated in propositional logic with 3 commuting S5 modalities, in
[S5,S5,S5]. There are many consequences, e.g., free finitely generated
Df3's are not atomic and [S5,S5,S5] has Godel's incompleteness property.

 

Thm.1. Set Theory can be built up in propositional logic with 3 commuting S5
modalities, or equivalently, in the equational theory EqDf3  of
3-dimensional diagonal-free cylindric algebras.

 

Thm.2.  First-order logic  L(omega,omega)  can be reduced to the
propositional logic [S5,S5,S5]. More precisely, let  T  be a theory of
L(omega,omega)  whose models are infinite. Then  T  admits a simple
conservative extension  T+  (via a single extra axiom) which in turn is
reducible to  [S5,S5,S5].

 

Detailed statements and proofs are available on Istvan’s home-page
http://www.renyi.hu/~nemeti/FormalizingST.htm , announcement is there since
this July  http://www.renyi.hu/~nemeti/NDis/formalizingsettheory.pdf and
preprint with complete proof since September 14,
http://www.renyi.hu/~nemeti/NDis/diagonalfree.pdf .

 

Istvan Nemeti and Hajnal Andreka

 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20111001/4cf95bb5/attachment.html>