|
|
Dear Alan
Thanks for your reply
>
> something wrong here --
> HA4 isn't even classically true (eg A true, B false, C false)
>
> presumably we want:
> (A-->B) --> ((B-->C) --> (A-->C))
>
I will have to look at heyting himself for the HA4 axiom.
But maybe this shows that Heyting wasn't so bothered about axioms at
all (a good intuistic principle)
>
> no; each of these systems has its own notion of inference rule, in
> addition to having the axioms, and we need to know the inference rules
> to know what proofs in the system look like. What should be true is
> that there is a proof of a statement using the axioms and inference
> rules in one case if and only if there is a proof of that statement
> using the other axioms and inference rules.
>
O this got confusing
there are different inference rules sets here:
the Axiom-inference-rule-set that concist of:
Modus ponens and Uniform substitution (nothing else)
and the Object-inference-rule-set that concists of all Natural
deduction rules for Intuistic logic.
The Question is:
Using only the Axiom-inference-rule-set prove that every
Object-inference-rule follows from some or all axioms.
Proving the Object-inference-rule set from the
Object-inference-rule-set is circular and leads to nothing usefull in
particular.
>
> with Heyting's axioms, to show A & B --> A,
> there should be a proof linking up
>
> (A & B) --> ((B --> A) & B) (from HA5 and HA3)
>
> ((B --> A) & B) --> (B & (B-->A)) HA2
>
> (B & (B-->A)) --> A HA6
>
>
That Doesn't seem to use the right interference rule set. i am
afraight.
But still thanks for your reply.
Gives me more to think about. and to clarify myself.
Alan Smaill wrote:
> "translogi@xxxxxxxxxxxxxx" <translogi@xxxxxxxxxxxxxx> writes:
>
> > |using only Heytings axuioms I am even unable to prove that
> > |
> > |(A & B) --> A
>
> ...
>
> > There seem to be (at least) two sets of axioms for intuitionistic
> > logic.
> >
> > The intuitionistic axioms from
> > http://en.wikipedia.org/wiki/Intuitionistic_logic
> >
> > THEN-1: A --> (B --> A)
> > THEN-2: (A --> (B --> C)) --> ((A --> B) --> (A --> C))
> > AND-1: A & B --> A
> > AND-2: A & B --> B
> > AND-3: A --> (B --> (A & B))
> > OR-1: A --> A v B
> > OR-2: B --> A v B
> > OR-3: (A --> C) --> ((B --> C) --> (A v B --> C))
> > NOT-1: (A --> B) --> ((A --> ~B) --> ~ A)
> > NOT-2: A --> (~A --> B)
> >
> >
> > The intuitionistic axiom set from Heyting
> > home.utah.edu/~nahaj/logic/structures/axioms/index.html#HA1">http://home.utah.edu/~nahaj/logic/structures/axioms/index.html#HA1
> >
> > HA1: A --> (A & A)
> > HA2: (A & B) --> (B & A)
> > HA3: (A-->B) --> ((A & C) --> (B & C))
> > HA4: ((A-->B) --> (B-->C)) --> (A-->C)
>
> something wrong here --
> HA4 isn't even classically true (eg A true, B false, C false)
>
> presumably we want:
> (A-->B) --> ((B-->C) --> (A-->C))
>
> > HA5: B --> (A-->B)
> > HA6: (A & (A-->B)) --> B
> > HA7: A --> (A v B)
> > HA8: (A v B) --> (B v A)
> > HA9: ((A-->C) & (B-->C)) --> ((A v B) -->C)
> > HA10: ~A --> (A-->B)
> > HA11: ((A-->B) & (A-->~B)) --> ~A
> >
> >
> > HA5 and THEN-1 are identical
> > HA7 and OR-1 are identical
> > HA9 and OR-3 are identical
> > HA11 and NOT-2 are identical
> >
> > But are these two sets allways saying the same thing?
>
> should be
>
> > With sufficient i mean:
> > Does the axioms prove the inference rules.
> > Or are the inference rules derivable from the axioms.
> > (I hope these two mean the same thing)
>
> no; each of these systems has its own notion of inference rule, in
> addition to having the axioms, and we need to know the inference rules
> to know what proofs in the system look like. What should be true is
> that there is a proof of a statement using the axioms and inference
> rules in one case if and only if there is a proof of that statement
> using the other axioms and inference rules.
>
> > axiom stelsel
> > Yes indeed I ment axiom system (I am dutch thats why)
> >
> > I am asking all this because I (re) discovered a new? kind of
> > sub-intuitionistic logic see another tread on sci.logic.
> > groups.google.com/group/sci.logic/browse_frm/thread/359b993f0bef4c22/#">http://groups.google.com/group/sci.logic/browse_frm/thread/359b993f0bef4c22/#
> >
> > and it is nice to have a proper axiom set for it.
> >
> > I could just use Heytingss one and replace
> > HA7 with A --> (A v ~B)
> > HA10 with ((A v B) & ~B) --> A
> > and add some axioms for cases not covered
> > but that just doesn't seem the right way to use it
>
> with Heyting's axioms, to show A & B --> A,
> there should be a proof linking up
>
> (A & B) --> ((B --> A) & B) (from HA5 and HA3)
>
> ((B --> A) & B) --> (B & (B-->A)) HA2
>
> (B & (B-->A)) --> A HA6
>
>
> --
> Alan Smaill
|
|