[FOM] Conservative Extensions of Logic

negri@mappi.helsinki.fi negri at mappi.helsinki.fi
Thu Feb 8 05:22:01 EST 2007

Dear Dr. Muller,

A proof of conservativity of predicate logic with equality over predicate 
logic can be found in our book "Structural Proof Theory", (CUP 2001, 
theorem 6.5.6, p. 141). The proof is based on the formulation of predicate 
logic in terms of sequent calculus. The equality axioms are converted into 
extra rules and conservativity follows from cut elimination.

We showed our proof to Anne Troelstra before it was published in our book. 
He was very pleased about it and asked to include it in the second edition 
of "Basic Proof Theory." (CUP, 2000). Thus, you find the proof-theoretic 
treatment of the matter also in that book.


Sara Negri & Jan von Plato

Lainaus "F.A.Muller" <F.A.Muller at phys.uu.nl>:

> Lectori Salutem,
> Does anyone know any papers of books where to
> find proofs of the following theorem. I am not
> 100% whether these actually are theorem; I have proofs
> of my own about which I am not wholly certain,
> which is why I ask: I'd like to compare them with
> what is known --- I really have consulted a lot of
> logic text-books, but all in vain.
> 1PL    : classical 1st-order predicate logic
>             (no matter how characterised precisely)
> 1PL+  : 1PL extended with the Frege axioms for
>              identity (reflexivity and substitutivity schema)
> Thm
> 1PL+ is a conservative extension of 1PL.
> Many thanks in advance,
> --> F.A. Muller
> *******************************************
> Dr F.A. Muller
> Institute for the History & Foundations of Science
> Dept. of Physics & Astronomy
> Utrecht University
> f.a.muller at phys.uu.nl
> &
> Fac. of Philosophy
> Erasmus University Rotterdam
> f.a.muller at fwb.eur.nl
> *******************************************
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

More information about the FOM mailing list