Re: Embedding classical logic theories into intuitionistic logic

On Aug 28, 8:20 am, David Libert <libert.da...@xxxxxxxxx> wrote:
This topic is of interest to me, as one way to viewintuitionistic
logic, to think of how it differs from classical logic by seeing how
it sits above a suitable fragment of itself interpreting classical
theories.

I recall that a big text book by Kleene has a section with theorems
a little bit like this, various mappings F of first order language to
itself with results if classical proves phi thenintuitionistic
proves F(phi).

I looked up Wikipedia on Kleene and they list texts Introduction to
Metamethamatics and Mathematical Logic. I suspect I am thinking
of Mathematical Logic.

I don't have those texts at hand now. So I think I just came up
with something like this on my own.

Sointuitionisticlogic has the idea, to prove a disjunction we
should prove a disjunct. Classical logic differs by allowing indirect
proofs of disjunctions. Similarly, intuitionisticlogic wants you
to prove an existential by proving at least a disjunction of specific
witnesses, while classical allows indirect proofs of existentials.
So these two logics treat disjunctions and existentials differently.

On the other hand, they are similar treating conjunction,
implication, and universal quantifiers.

In intuitionist logic, we can get something similar to the
classical (A or B) by ~(A & B), ie we can do indirect proofs of
that version right inintuitionisticlogic.

So suggested by all this, I think I found a proof of the following
theorem about pure theorems of the logic, (only the axioms of =
over the pure logic, no non-logical axioms).

In fact I end up treating -> as bad too, not from the original
consideration but from doing the proof.

Suppose phi is a formula with no v ,-> or existentials, and
only having atomics, ~, & and universal quatnifiers. Then pure
classical logic |- phi <-> pure intutitionistic logic |- phi.

So in other words, if you re-write all disjunctions as ~ ( & )
and all existentials as ~ all ~,
then this classical version has the logics agreeing.

So one way to think of the relations of the pure logics (if I
haven't made a mistake in that proof and the result is really true etc
etc) is you could say things are "really" in the widest view
intutionistic, and classical logic is just confining itself to that
fragment, and think of the classical v , exist as abbreviations
for that version.

Coming up with a version like this for applied theoriwes with non-
logical axioms is trickier, but I think I found something. To get
started we have to first consider classical theories of a specific
restricted form. I will later comment how to represent arbitrary
theories into this form.

So fr the special form first. Consider an axiom set A for a
classical first order theory, ie A being thwe set of non-logical
axioms which will be used with the pure logical axioms and rules of
inference. To make a result like this, I had to consider a specific
classical version of the axioms, choosing among classically
equivalent. Namely we must assume the axioms of A have been written
in a classical form of positive formulas: v & -> exists all are
allowed, but no ~ are allowed.

So as i say, sometimes this will be impossible. We can pull `
inside through other conenctives and quantifiers, and cancel double
negations, but by the end of this, we might get single ~ on some
atomic formulas.

So the starting version of this is axiomatizations that get no such
~.

So the base result (again modulo errors etc) is if A has been
successfully put into that form and (here is the odd point to let a
theorem like this work) conclusion phi is in the OTHER form : ~
allowed but no v exist, then if A |- classically phi
then A |- intuitionistically phi.

So for axiomatizations of this special form, one way to think of
classical logic is it is working inside of intutionistic logic but
confining itself to results of this special form above, this weird
mixed form where we formulate axioms and theorems differently.

So how to relate an arbitrary classical theorem to the above? Given
an arbitrary classical axiomatization, pull negations inside like i
said above. Where the resulting formula has single negations on an
atomic formula B : ~Bx1...xn, make a new predicate symbol NB and
replace ~Bx1...xn by NBx1...xn.

For each such newly created symbol add axioms (in the proper form
for axiomatizations we require):
all x1...xn (Bx1...xn v NBx1...xn)
and a schematum of axioms for formulas in the proper form we are
considering, all such formulas theta of the langauge (theta allowed
to have free variables among the x1...xn) :

all x1...xn [ (Bx1...xn & NBx1...xn) -> theta ].

If the original form of the A's with ~B proves phi as form of
comclusion above classically, then classically the new form of A with
the NB 's and those axioms proves phi.

So this is sort of a representation in the special form of the the
original classical theory.

I think many theories will already be of this positive form. But if
not we can recast them as above. Then consider the resulting
classical theory insideintuitionisticas above.

Using v, -> exists inituitionistically is strong. Claiming to
prove those intuitionistically is claiming to have constructive proofs
with respect to those.

On the other hand, replacing v , ->, exists by their classical
equivalents using ~, & , all is weak, it can be done by indirect
proofs inintuitionisticlogic.

So to make a version givingintuitionistican easy job to try to
duplicate classical, we put the premises in strong form and the
conclusion in weak form.

This was inspired by a recent post of Keith Ramsay in another
thread, where he said intuitonistic logic has a different
interpretation of the connectives than classical. This led me to
wonder, can we make a mixed logic with both a classical and
intitutionistic versions of those connectives as separate connectives,
and an overall mixed logic so the purely intutionisitic formulas act
like intuitionisitic logic and the purely classical ones act like
classical.

I had tried this before, but if you put in the usual natural
deduction rules for classical ~, it makes the intutionistic
conenctives collapse back to classical. Then it occurred to me to
make a version where the classical connectives only behave classically
when all subformulas are purely classical. From there it occurred to
me I was more or less making a classical fragment inside intuitionism
directly, so I may as well use intutionism's representation of the
classical.

A preliminary attempt at this, I thought maybe all we needed to do
was pull all negations inside axioms, so phrase axioms as positive
combinations over atomics and negations atomics. But that has the
counterexample; axiom ~Pa -> Pa, with phi the classical
theorem Pa, but inituitionism onyl proves ~~Pa from that axiom.

So I came up with the form, no negations, even on atomics.

--
David Libert

Interesting tread.

Just some short remarks

if classical logic proves A
intuitionistic logic can prove ~~A.

if classical logic proves ~ A
intuitionistic logic can prove ~A.

If intuitionistic logic proves A.
classical logic can prove A

If intuitionistic logic proves ~A.
classical logic can prove ~A

If intuitionistic logic proves ~~A.
classical logic can prove A

the exsistential is quite a different kettle of fish.
I will have to read it again but i think that (UNFORTUNEDLY)
the "for all" quantifieer is the primitive real one.
the"there is" is just a defined connective. {Not (for all) not}

I will look it up in my copy of Heytings famous aricle. (witch also
very unfiortuedly is only in german and not even online)

Will come back to you






.

Relevant Pages

  • Re: Do we really need to have models for a theory?
    ... >>> entirety just goes to infinitely higher order logics. ... >> be associated with large cardinal axioms. ... > Hi Mitch, ... > being the one infinite set. ...
    (sci.logic)
  • Re: tedious sledding re set existence in FOL
    ... >>> That involves NO axioms. ... It involves inference rules INSTEAD OF ... > classical logics are all sufficiently different from ... the theorem is a proven, no matter what semantics we choose, even if, ...
    (sci.logic)
  • Re: Analytic/Synthetic distinction in modern inference engines?
    ... You asked about the analytic/synthetic distinction, ... to ask about logics that treat the a/s distinction in some interesting ... All you have to do is pick appropriate axioms for whatever field ... preexisting axioms) can conflict with that; ...
    (sci.logic)
  • Re: Analytic/Synthetic distinction in modern inference engines?
    ... Since they ARE logics, ... pile up new knowledge (new axioms). ... That IS NOT the analytic/synthetic distinction. ... What you ACTUALLY want is a framework wherein ...
    (sci.logic)
  • Embedding classical logic theories into intuitionistic logic
    ... itself with results if classical proves phi then intuitionistic ... So these two logics treat disjunctions and existentials differently. ... over the pure logic, no non-logical axioms). ... me I was more or less making a classical fragment inside intuitionism ...
    (sci.logic)