Hello I see different lists of what the axioms of intuitionistic logic
are.
Can somebody enlighten me in this?
expecially is Modes Tollens
(p ->q) -> (-q -> -p) an axiom or not ?
also are there standard rules in Gentzens NJ sequents?
Thanks in advance
transl…@googlemail.com wrote:
> (p ->q) -> (-q -> -p) an axiom or not ?
It may or may not be an axiom depending on the particular
axiomatization. In any case, it is a theorem. But (~P -> ~Q) -> (Q ->
P) is not a theorem.
MoeBlee
MoeBlee wrote:
> transl…@googlemail.com wrote:
> > (p ->q) -> (-q -> -p) an axiom or not ?
> It may or may not be an axiom depending on the particular
> axiomatization. In any case, it is a theorem. But (~P -> ~Q) -> (Q ->
> P) is not a theorem.
> MoeBlee
(p ->q) = (-q -> -p) is a theorem on Logic Algebra. That is to say (p
->q) -> (-q -> -p) and (-q -> -p) -> (p ->q) are all theorem on Logic
algebra. You can use the axioms on Logic algebra to prove it.
conbra
Conbra wrote:
> MoeBlee wrote:
> > transl…@googlemail.com wrote:
> > > (p ->q) -> (-q -> -p) an axiom or not ?
> > It may or may not be an axiom depending on the particular
> > axiomatization. In any case, it is a theorem. But (~P -> ~Q) -> (Q ->
> > P) is not a theorem.
> > MoeBlee
> (p ->q) = (-q -> -p) is a theorem on Logic Algebra. That is to say (p
> ->q) -> (-q -> -p) and (-q -> -p) -> (p ->q) are all theorem on Logic
> algebra. You can use the axioms on Logic algebra to prove it.
That’s nice. Meanwhile, (~P -> ~Q) -> (Q -> P) is not a theorem of
intuitionistic logic.
MoeBlee
It is as in classical logic. You can
have different axiom sets which yield
the same.
The full set is typically, call this
system A1 which is made up of (A),
(D) and (M):
(A) A |- A
(D) G |- B =>
G\A |- A->B
(M) G |- A->B &
H |- A =>
GuH |- B
Proof trees can be expressed by typed
lambda expressions. This leads to the curry
horward isomorphism:
(A’) x:A => x:A
(D’) t:B, x:A => lambda x t:A->B
(M’) t:A->B, s:A => (t s):B
One can either eliminate the rule (D)
or the rule (M).
Eliminating the rule (D) corresponds
to eliminating lambda abstraction
from lambda calculus. Which can be
done via the combinators S, K, I.
(I’) lambda x x
(K’) lambda y lambda x y
(S’) lambda x lambda y lambda z (x z)(y z)
If one looks at the typing of these
combinators, one finds the following
new axioms. We can call this the
system A2, it is made up of (A),
(M), (I), (K) and (S):
(I) A->A
(K) B->(A->B)
(S) (A->(B->C))->((A->B)->(A->C))
The rule (M) is not analytic, it introduces
a new formula A. It can be eliminated
similiar to forming a normal form
of a lambda expression. A normal form
term will either the form:
(x r_1 .. r_n) or
(lambda x r)
Where r_1, .., r_n, r are again in
normal form. A further analysis reveals
that we can replace (M) by the following
rule (R) which is now analytic:
(R) G1 |- A1 &
..
& Gn |- An =>
G1 u .. u Gn u A1->..An->B |- B
Thus another axiom set would be A3,
consiting of (I), (D) and (R).
Lets make a little exercise, lets try
to proof the sylogism in intutionistc
logic, i.e. lets try to proof:
(A->B)->((B->C)->(A->C))
We use axiom set (A3) first:
1 A |- A (I)
2 A->B, A |- B (R) on 1
3 A->B, B->C, A |- C (R) on 2
4 A->B, B->C |- A->C (D) on 3
5 A->B |- (B->C)->(A->C) (D) on 4
6 |- (A->B)->((B->C)->(A->C)) (D) on 5
Lets see what the lambda expression of this
proof is.
1 x:A => x:A
2 y:A->B, x:A => (y x):B
3 y:A->B, z:B->C, x:A => (z (y x)):C
4 y:A->B, z:B->C, x:A => lambda x (z (y x)):A->C
5 y:A->B, z:B->C, x:A => lambda z lambda x (z (y x)):(B->C)->(A->C)
6 y:A->B, z:B->C, x:A => lambda y lambda z lambda x (z (y x)):
(A->B)->((B->C)->(A->C))
We can use this expression to construct a proof
in (A1) and (A2). The proof in (A1) looks as
follows, we simple replace lambdas by (D)
and application by (M):
1 A |- A (I)
2 A->B |- A->B (I)
3 B->C |- B->C (I)
4 A->B, A |- B (M) on 1, 2
5 A->B, B->C, A |- C (M) on 4,3
6 A->B, B->C |- A->C (D) on 5
7 A->B |- (B->C)->(A->C) (D) on 6
8 |- (A->B)->((B->C)->(A->C)) (D) on 7
The proof in (A2) looks as follows. We first transform
the lambda expression for the proof into combinatorials.
We simply (sic!) replace lambdas by S, K and I. We get:
lambda y lambda z lambda x (z (y x)) = s (s (k s) (s (s (k s) (s (k
k) (k s))) (s (s (k s) (s (k k) (k k))) (k i)))) (s (s (k s) (s (s (k s)
(s (k k) (k s))) (s (s (k s) (s (k k) (k k))) (s (k k) i)))) (s (k k) (k
i)))
Thus a proof of the syllogism in A2 would look
as follows, after even eliminating redundant
proof steps:
1 ax s:
(((A->B)->(((B->C)->(A->B))->((B->C)->(A->C))))->(((A->B)->((B->C)->(A->B)))->((A->B)->((B->C)->(A->C)))))
2 ax s:
(((A->B)->(((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C)))))->(((A->B)->((B->C)->((A->B)->(A->C))))->((A->B)->(((B->C)->(A->B))->((B->C)->(A->C))))))
3 ax k:
((((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C))))->((A->B)->(((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C))))))
4 ax s: (((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C))))
5 mp 3, 4:
((A->B)->(((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C)))))
6 mp 2, 5:
(((A->B)->((B->C)->((A->B)->(A->C))))->((A->B)->(((B->C)->(A->B))->((B->C)->(A->C)))))
7 ax s:
(((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))->(((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((A->B)->(A->C))))))
8 ax s:
(((A->B)->(((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C))))))->(((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))->((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))))
9 ax k:
((((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))->((A->B)->(((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))))
10 ax s:
(((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))
11 mp 9, 10:
((A->B)->(((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C))))))
12 mp 8, 11:
(((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))->((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C))))))
13 ax s:
(((A->B)->(((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C))))))->(((A->B)->((A->(B->C))->((A->B)->(A->C))))->((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))))
14 ax k:
((((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C)))))->((A->B)->(((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C)))))))
15 ax k:
(((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C)))))
16 mp 14, 15:
((A->B)->(((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C))))))
17 mp 13, 16:
(((A->B)->((A->(B->C))->((A->B)->(A->C))))->((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C))))))
18 ax k:
(((A->(B->C))->((A->B)->(A->C)))->((A->B)->((A->(B->C))->((A->B)->(A->C)))))
19 ax s: ((A->(B->C))->((A->B)->(A->C)))
20 mp 18, 19: ((A->B)->((A->(B->C))->((A->B)->(A->C))))
21 mp 17, 20: ((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))
22 mp 12, 21: ((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))
23 mp 7, 22:
(((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((A->B)->(A->C)))))
24 ax s:
(((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))->(((A->B)->((B->C)->(B->C)))->((A->B)->((B->C)->(A->(B->C))))))
25 ax s:
(((A->B)->(((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C))))))->(((A->B)->((B->C)->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))))
26 ax k:
((((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))))
27 ax s:
(((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))
28 mp 26, 27:
((A->B)->(((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C))))))
29 mp 25, 28:
(((A->B)->((B->C)->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C))))))
30 ax s:
(((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C))))))->(((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((B->C)->(A->(B->C)))))))
31 ax k:
((((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C)))))))
32 ax k: (((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C)))))
33 mp 31, 32:
((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C))))))
34 mp 30, 33:
(((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((B->C)->(A->(B->C))))))
35 ax k: (((B->C)->(A->(B->C)))->((A->B)->((B->C)->(A->(B->C)))))
36 ax k: ((B->C)->(A->(B->C)))
37 mp 35, 36: ((A->B)->((B->C)->(A->(B->C))))
38 mp 34, 37: ((A->B)->((B->C)->((B->C)->(A->(B->C)))))
39 mp 29, 38: ((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))
40 mp 24, 39: (((A->B)->((B->C)->(B->C)))->((A->B)->((B->C)->(A->(B->C)))))
41 ax k: (((B->C)->(B->C))->((A->B)->((B->C)->(B->C))))
42 ax i: ((B->C)->(B->C))
43 mp 41, 42: ((A->B)->((B->C)->(B->C)))
44 mp 23, 37: ((A->B)->((B->C)->((A->B)->(A->C))))
45 mp 6, 44: ((A->B)->(((B->C)->(A->B))->((B->C)->(A->C))))
46 mp 1, 45: (((A->B)->((B->C)->(A->B)))->((A->B)->((B->C)->(A->C))))
47 ax s:
(((A->B)->(((B->C)->(A->A))->((B->C)->(A->B))))->(((A->B)->((B->C)->(A->A)))->((A->B)->((B->C)->(A->B)))))
48 ax s:
(((A->B)->(((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B)))))->(((A->B)->((B->C)->((A->A)->(A->B))))->((A->B)->(((B->C)->(A->A))->((B->C)->(A->B))))))
49 ax k:
((((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B))))->((A->B)->(((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B))))))
50 ax s: (((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B))))
51 mp 49, 50:
((A->B)->(((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B)))))
52 mp 48, 51:
(((A->B)->((B->C)->((A->A)->(A->B))))->((A->B)->(((B->C)->(A->A))->((B->C)->(A->B)))))
53 ax s:
(((A->B)->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B)))))->(((A->B)->((B->C)->(A->(A->B))))->((A->B)->((B->C)->((A->A)->(A->B))))))
54 ax s:
(((A->B)->(((B->C)->((A->(A->B))->((A->A)->(A->B))))->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B))))))->(((A->B)->((B->C)->((A->(A->B))->((A->A)->(A->B)))))->((A->B)->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B)))))))
55 ax k:
((((B->C)->((A->(A->B))->((A->A)->(A->B))))->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B)))))->((A->B)->(((B->C)->((A->(A->B))->((A->A)->(A->B))))->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B)))))))
56 ax s:
(((B->C)->((A->(A->B))->((A->A)->(A->B))))->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B)))))
57 mp 55, 56:
((A->B)->(((B->C)->((A->(A->B))->((A->A)->(A->B))))->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B))))))
58 mp 54, 57:
(((A->B)->((B->C)->((A->(A->B))->((A->A)->(A->B)))))->((A->B)->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B))))))
59 ax s:
(((A->B)->(((A->(A->B))->((A->A)->(A->B)))->((B->C)->((A->(A->B))->((A->A)->(A->B))))))->(((A->B)->((A->(A->B))->((A->A)->(A->B))))->((A->B)->((B->C)->((A->(A->B))->((A->A)->(A->B)))))))
…
read more »
- Hide quoted text — Show quoted text -
On Fri, 8 Sep 2006, MoeBlee wrote:
> Conbra wrote:
> > MoeBlee wrote:
> > > transl…@googlemail.com wrote:
> > > > (p ->q) -> (-q -> -p) an axiom or not ?
> > > It may or may not be an axiom depending on the particular
> > > axiomatization. In any case, it is a theorem. But (~P -> ~Q) -> (Q ->
> > > P) is not a theorem.
> > (p ->q) = (-q -> -p) is a theorem on Logic Algebra. That is to say (p
> > ->q) -> (-q -> -p) and (-q -> -p) -> (p ->q) are all theorem on Logic
> > algebra. You can use the axioms on Logic algebra to prove it.
> That’s nice. Meanwhile, (~P -> ~Q) -> (Q -> P) is not a theorem of
> intuitionistic logic.
Irrevalent. Concept or logic algebra, which Conbra won’t explain to us in
simple easy to read manner, is being promoted by him as the only logic
worthy of the logical universe. Thus your rebuke of Conbra for ignoring
that OP’s question was about intuitionistic logic, is illogical concept
algebra. Tho this may seem unintuitive, it computes with logic algebra.
My understanding of intuitionistic logic is that it’s natural deduction
with natural negation and the axiom,
contradiction implies any statement
When Curry discovered Schönfinkel
http://www.sadl.uleth.ca/gsdl/cgi-bin/library?e=d-000-00—0curry–00...
- Hide quoted text — Show quoted text -
Jan Burse wrote:
> It is as in classical logic. You can
> have different axiom sets which yield
> the same.
> The full set is typically, call this
> system A1 which is made up of (A),
> (D) and (M):
> (A) A |- A
> (D) G |- B =>
> G\A |- A->B
> (M) G |- A->B &
> H |- A =>
> GuH |- B
> Proof trees can be expressed by typed
> lambda expressions. This leads to the curry
> horward isomorphism:
> (A’) x:A => x:A
> (D’) t:B, x:A => lambda x t:A->B
> (M’) t:A->B, s:A => (t s):B
> One can either eliminate the rule (D)
> or the rule (M).
> Eliminating the rule (D) corresponds
> to eliminating lambda abstraction
> from lambda calculus. Which can be
> done via the combinators S, K, I.
> (I’) lambda x x
> (K’) lambda y lambda x y
> (S’) lambda x lambda y lambda z (x z)(y z)
> If one looks at the typing of these
> combinators, one finds the following
> new axioms. We can call this the
> system A2, it is made up of (A),
> (M), (I), (K) and (S):
> (I) A->A
> (K) B->(A->B)
> (S) (A->(B->C))->((A->B)->(A->C))
> The rule (M) is not analytic, it introduces
> a new formula A. It can be eliminated
> similiar to forming a normal form
> of a lambda expression. A normal form
> term will either the form:
> (x r_1 .. r_n) or
> (lambda x r)
> Where r_1, .., r_n, r are again in
> normal form. A further analysis reveals
> that we can replace (M) by the following
> rule (R) which is now analytic:
> (R) G1 |- A1 &
> ..
> & Gn |- An =>
> G1 u .. u Gn u A1->..An->B |- B
> Thus another axiom set would be A3,
> consiting of (I), (D) and (R).
> Lets make a little exercise, lets try
> to proof the sylogism in intutionistc
> logic, i.e. lets try to proof:
> (A->B)->((B->C)->(A->C))
> We use axiom set (A3) first:
> 1 A |- A (I)
> 2 A->B, A |- B (R) on 1
> 3 A->B, B->C, A |- C (R) on 2
> 4 A->B, B->C |- A->C (D) on 3
> 5 A->B |- (B->C)->(A->C) (D) on 4
> 6 |- (A->B)->((B->C)->(A->C)) (D) on 5
> Lets see what the lambda expression of this
> proof is.
> 1 x:A => x:A
> 2 y:A->B, x:A => (y x):B
> 3 y:A->B, z:B->C, x:A => (z (y x)):C
> 4 y:A->B, z:B->C, x:A => lambda x (z (y x)):A->C
> 5 y:A->B, z:B->C, x:A => lambda z lambda x (z (y x)):(B->C)->(A->C)
> 6 y:A->B, z:B->C, x:A => lambda y lambda z lambda x (z (y x)):
> (A->B)->((B->C)->(A->C))
> We can use this expression to construct a proof
> in (A1) and (A2). The proof in (A1) looks as
> follows, we simple replace lambdas by (D)
> and application by (M):
> 1 A |- A (I)
> 2 A->B |- A->B (I)
> 3 B->C |- B->C (I)
> 4 A->B, A |- B (M) on 1, 2
> 5 A->B, B->C, A |- C (M) on 4,3
> 6 A->B, B->C |- A->C (D) on 5
> 7 A->B |- (B->C)->(A->C) (D) on 6
> 8 |- (A->B)->((B->C)->(A->C)) (D) on 7
> The proof in (A2) looks as follows. We first transform
> the lambda expression for the proof into combinatorials.
> We simply (sic!) replace lambdas by S, K and I. We get:
> lambda y lambda z lambda x (z (y x)) = s (s (k s) (s (s (k s) (s (k
> k) (k s))) (s (s (k s) (s (k k) (k k))) (k i)))) (s (s (k s) (s (s (k s)
> (s (k k) (k s))) (s (s (k s) (s (k k) (k k))) (s (k k) i)))) (s (k k) (k
> i)))
> Thus a proof of the syllogism in A2 would look
> as follows, after even eliminating redundant
> proof steps:
> 1 ax s:
> (((A->B)->(((B->C)->(A->B))->((B->C)->(A->C))))->(((A->B)->((B->C)->(A->B)))->((A->B)->((B->C)->(A->C)))))
> 2 ax s:
> (((A->B)->(((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C)))))->(((A->B)->((B->C)->((A->B)->(A->C))))->((A->B)->(((B->C)->(A->B))->((B->C)->(A->C))))))
> 3 ax k:
> ((((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C))))->((A->B)->(((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C))))))
> 4 ax s: (((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C))))
> 5 mp 3, 4:
> ((A->B)->(((B->C)->((A->B)->(A->C)))->(((B->C)->(A->B))->((B->C)->(A->C)))))
> 6 mp 2, 5:
> (((A->B)->((B->C)->((A->B)->(A->C))))->((A->B)->(((B->C)->(A->B))->((B->C)->(A->C)))))
> 7 ax s:
> (((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))->(((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((A->B)->(A->C))))))
> 8 ax s:
> (((A->B)->(((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C))))))->(((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))->((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))))
> 9 ax k:
> ((((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))->((A->B)->(((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))))
> 10 ax s:
> (((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))
> 11 mp 9, 10:
> ((A->B)->(((B->C)->((A->(B->C))->((A->B)->(A->C))))->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C))))))
> 12 mp 8, 11:
> (((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))->((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C))))))
> 13 ax s:
> (((A->B)->(((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C))))))->(((A->B)->((A->(B->C))->((A->B)->(A->C))))->((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))))
> 14 ax k:
> ((((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C)))))->((A->B)->(((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C)))))))
> 15 ax k:
> (((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C)))))
> 16 mp 14, 15:
> ((A->B)->(((A->(B->C))->((A->B)->(A->C)))->((B->C)->((A->(B->C))->((A->B)->(A->C))))))
> 17 mp 13, 16:
> (((A->B)->((A->(B->C))->((A->B)->(A->C))))->((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C))))))
> 18 ax k:
> (((A->(B->C))->((A->B)->(A->C)))->((A->B)->((A->(B->C))->((A->B)->(A->C)))))
> 19 ax s: ((A->(B->C))->((A->B)->(A->C)))
> 20 mp 18, 19: ((A->B)->((A->(B->C))->((A->B)->(A->C))))
> 21 mp 17, 20: ((A->B)->((B->C)->((A->(B->C))->((A->B)->(A->C)))))
> 22 mp 12, 21: ((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((A->B)->(A->C)))))
> 23 mp 7, 22:
> (((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((A->B)->(A->C)))))
> 24 ax s:
> (((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))->(((A->B)->((B->C)->(B->C)))->((A->B)->((B->C)->(A->(B->C))))))
> 25 ax s:
> (((A->B)->(((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C))))))->(((A->B)->((B->C)->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))))
> 26 ax k:
> ((((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))))
> 27 ax s:
> (((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))
> 28 mp 26, 27:
> ((A->B)->(((B->C)->((B->C)->(A->(B->C))))->(((B->C)->(B->C))->((B->C)->(A->(B->C))))))
> 29 mp 25, 28:
> (((A->B)->((B->C)->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C))))))
> 30 ax s:
> (((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C))))))->(((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((B->C)->(A->(B->C)))))))
> 31 ax k:
> ((((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C)))))->((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C)))))))
> 32 ax k: (((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C)))))
> 33 mp 31, 32:
> ((A->B)->(((B->C)->(A->(B->C)))->((B->C)->((B->C)->(A->(B->C))))))
> 34 mp 30, 33:
> (((A->B)->((B->C)->(A->(B->C))))->((A->B)->((B->C)->((B->C)->(A->(B->C))))))
> 35 ax k: (((B->C)->(A->(B->C)))->((A->B)->((B->C)->(A->(B->C)))))
> 36 ax k: ((B->C)->(A->(B->C)))
> 37 mp 35, 36: ((A->B)->((B->C)->(A->(B->C))))
> 38 mp 34, 37: ((A->B)->((B->C)->((B->C)->(A->(B->C)))))
> 39 mp 29, 38: ((A->B)->(((B->C)->(B->C))->((B->C)->(A->(B->C)))))
> 40 mp 24, 39: (((A->B)->((B->C)->(B->C)))->((A->B)->((B->C)->(A->(B->C)))))
> 41 ax k: (((B->C)->(B->C))->((A->B)->((B->C)->(B->C))))
> 42 ax i: ((B->C)->(B->C))
> 43 mp 41, 42: ((A->B)->((B->C)->(B->C)))
> 44 mp 23, 37: ((A->B)->((B->C)->((A->B)->(A->C))))
> 45 mp 6, 44: ((A->B)->(((B->C)->(A->B))->((B->C)->(A->C))))
> 46 mp 1, 45: (((A->B)->((B->C)->(A->B)))->((A->B)->((B->C)->(A->C))))
> 47 ax s:
> (((A->B)->(((B->C)->(A->A))->((B->C)->(A->B))))->(((A->B)->((B->C)->(A->A)))->((A->B)->((B->C)->(A->B)))))
> 48 ax s:
> (((A->B)->(((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B)))))->(((A->B)->((B->C)->((A->A)->(A->B))))->((A->B)->(((B->C)->(A->A))->((B->C)->(A->B))))))
> 49 ax k:
> ((((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B))))->((A->B)->(((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B))))))
> 50 ax s: (((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B))))
> 51 mp 49, 50:
> ((A->B)->(((B->C)->((A->A)->(A->B)))->(((B->C)->(A->A))->((B->C)->(A->B)))))
> 52 mp 48, 51:
> (((A->B)->((B->C)->((A->A)->(A->B))))->((A->B)->(((B->C)->(A->A))->((B->C)->(A->B)))))
> 53 ax s:
> (((A->B)->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B)))))->(((A->B)->((B->C)->(A->(A->B))))->((A->B)->((B->C)->((A->A)->(A->B))))))
> 54 ax s:
> (((A->B)->(((B->C)->((A->(A->B))->((A->A)->(A->B))))->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B))))))->(((A->B)->((B->C)->((A->(A->B))->((A->A)->(A->B)))))->((A->B)->(((B->C)->(A->(A->B)))->((B->C)->((A->A)->(A->B)))))))
> 55 ax k:
…
read more »
In intuitionistic logic, the
following is not valid
(pierce formula):
((P->Q)->P)->P (1)
It is neither provable
in via the systems (A1),
(A2) or (A3).
In (A3) we can even show
that it is not provable,
via some inversion lemmas
on (A3).
I assume (1) is provable
in conbras logic, so that
this logic is not intuitionistic.
There are many many formulas
valid in classical but
not in intuitionistic logic.
Bye
- Hide quoted text — Show quoted text -
Conbra wrote:
> MoeBlee wrote:
>>transl…@googlemail.com wrote:
>>>(p ->q) -> (-q -> -p) an axiom or not ?
>>It may or may not be an axiom depending on the particular
>>axiomatization. In any case, it is a theorem. But (~P -> ~Q) -> (Q ->
>>P) is not a theorem.
>>MoeBlee
> (p ->q) = (-q -> -p) is a theorem on Logic Algebra. That is to say (p
> ->q) -> (-q -> -p) and (-q -> -p) -> (p ->q) are all theorem on Logic
> algebra. You can use the axioms on Logic algebra to prove it.
> conbra
William Elliot wrote:
> Thus your rebuke of Conbra
I didn’t rebuke him.
MoeBlee
transl…@googlemail.com wrote:
> Hello I see different lists of what the axioms of intuitionistic logic
> are.
> Can somebody enlighten me in this?
> expecially is Modes Tollens
> (p ->q) -> (-q -> -p) an axiom or not ?
> also are there standard rules in Gentzens NJ sequents?
> Thanks in advance
Yes, it is an axiom (or theorem), but as mentioned, its converse is
not.
Take any axiomatization of the propositional calculus. The
intuitionistic calculus can be obtained from it by replacing its axioms
governing negation with weaker ones. Hence intuitionistic logic is a
sublogic of classical logic.
Without actually providing an axiomatization of it, here are some
formulas that are not valid in intuitionistic logic.
1. ~~p -> p [double negation elimination]
2. p v ~p [excluded middle]
3. ~(p & q) = (~p v ~q) [de morgan's over conjunction]
4. ~(p v q) = (~p & ~q) [de morgan's over disjunction]
5. (p -> q) = ~(p & ~q)
Some that are valid are:
6. (p -> ~p) -> ~p [reductio ad absurdum]
7. ~p -> (p -> q) [denial of antecedent]
8. (p -> q) -> ((p -> ~q) -> ~p) [reductio ad absurdum]
9. p -> ~~p [double negation introduction]
10. ~…~p -> ~p [special law of negation elimination] for odd n>2
occurrences of ‘~’ in the antecedent.
On Mon, 11 Sep 2006, MoeBlee wrote:
> William Elliot wrote:
> > Thus your rebuke of Conbra
> I didn’t rebuke him.
As best as I can recollect, I may have meant to say,
"Thus your rebuke from Conbra."
transl…@googlemail.com wrote:
Axioms, and a whole lot of other interesting stuff, can be found here:
http://www.seop.leeds.ac.uk/entries/logic-intuitionistic/. Dummett’s
book: http://www.oup.com/uk/catalogue/?ci=9780198505242 is a good read.
–
Remove "antispam" and ".invalid" for e-mail address.
William Elliot wrote:
> As best as I can recollect, I may have meant to say,
> "Thus your rebuke from Conbra."
But he didn’t rebuke me either. It’s not a big matter, though. Thanks.
MoeBlee
The system they show on:
http://www.seop.leeds.ac.uk/entries/logic-intuitionistic/
Corresponds to the system A3 I presented.
Thus to proof:
(A->B)->((B->C)->(A->C))
You need an aproximately ~100 steps proof,
instead of a ~10 step proof in A1 and A2.
But this is just a first guess. I didn’t
try the system on the seop link, which is
a copy of a stanford entry I think.
I only looked at the first axioms, which were:
A -> (B -> A). (1)
(A -> B) -> ((A -> (B -> C)) -> (A -> C)). (2)
(1) corresponds to the (K) rule in A3. (2)
corresponds to the (S) rule in A3. Unfortunately
the (I) rule is missing.
But the (I) rule is not necessary, because:
(s k k) = i
Interestingly if we try to proof the following
form of syllogism (note (A->B) and (B->C) have
changed sides):
(B->C)->((A->B)->(A->C))
Then we get a simpler proof than the ~100 lines
monster, because:
(s (k s) k):(B->C)->((A->B)->(A->C))
Namely the proof is:
1 ax s:
(((A->B)->((C->(A->B))->((C->A)->(C->B))))->(((A->B)->(C->(A->B)))->((A->B)->((C->A)->(C->B)))))
2 ax k:
(((C->(A->B))->((C->A)->(C->B)))->((A->B)->((C->(A->B))->((C->A)->(C->B)))))
3 ax s: ((C->(A->B))->((C->A)->(C->B)))
4 mp 2, 3: ((A->B)->((C->(A->B))->((C->A)->(C->B))))
5 mp 1, 4: (((A->B)->(C->(A->B)))->((A->B)->((C->A)->(C->B))))
6 ax k: ((A->B)->(C->(A->B)))
7 mp 5, 6: ((A->B)->((C->A)->(C->B)))
See also:
http://en.wikipedia.org/wiki/Curry-Howard_correspondence
Further:
According to following writer:
http://en.wikipedia.org/wiki/Implicational_propositional_calculus
It is enough to add the following axiom schema
to the system (A3) to arrive at an inference
system that is complete for classical
logic. The axiom schema that needs added
is Peirce’s law:
((P->Q)->P)->P (P)
I didn’t veriy the claim from the writer.
Also there was once a thread in sci.logic
that asked for other possible axioms, that
would introduce classicality into intuitionistic
logic.
Bye
- Hide quoted text — Show quoted text -
Frederick Williams wrote:
> transl…@googlemail.com wrote:
> Axioms, and a whole lot of other interesting stuff, can be found here:
> http://www.seop.leeds.ac.uk/entries/logic-intuitionistic/. Dummett’s
> book: http://www.oup.com/uk/catalogue/?ci=9780198505242 is a good read.
I just noticed, there is another system
(A4) which is probably a little bit
easier to handle than my (A2) with the
(R) rule. Instead of the (R) rule, the
(A4) has the following rule:
(L) G |- A,
D, B |- C =>
G,D, A->B |- C
It is the counterpart to (D). D is
sometimes called right -> introduction.
(L) can be called left -> introduction.
One can easily see that (L) implies
the (R) rule. The (R) rules is just
multiple applications of the (L) rule.
But the other direction is not direct,
can only be shown via the system (A1),
and then to go from (A1) to (A2) via
normalization of typed lambda expressions.
The system (A4) is nice, because also
it is analytical, that is no new formulas
are introduced during a proof.
The proof term corresponding to the
rule (L) is:
t:A, y:B, s:C, x:A->B =>
(lambda y s)(x t)
Thus we have shown how we can convert
(A4) proofs to (A1) proofs. Just
rewrite the proof, via the proof
term for (L)!
Lets make a little excercise with (L).
Lets try to proof peirce formula:
((P->Q)->P)->P
We use the proof system backwards,
starting from a hypothetic proof
step n, going back n-1, n-2, etc..
n: |- ((P->Q)->P)->P D on n-1
n-1: (P->Q)->P |- P L on n-3 and n-2
n-2: P |- P A
n-3: |- P->Q D on n-4
n-4: P |- Q <dead end>
So the peirce formula cannot be
proofed in system (A4).
Bye
- Hide quoted text — Show quoted text -
Jan Burse wrote:
> It is as in classical logic. You can
> have different axiom sets which yield
> the same.
> The full set is typically, call this
> system A1 which is made up of (A),
> (D) and (M):
> (A) A |- A
> (D) G |- B =>
> G\A |- A->B
> (M) G |- A->B &
> H |- A =>
> GuH |- B
> Proof trees can be expressed by typed
> lambda expressions. This leads to the curry
> horward isomorphism:
> (A’) x:A => x:A
> (D’) t:B, x:A => lambda x t:A->B
> (M’) t:A->B, s:A => (t s):B
> One can either eliminate the rule (D)
> or the rule (M).
> Eliminating the rule (D) corresponds
> to eliminating lambda abstraction
> from lambda calculus. Which can be
> done via the combinators S, K, I.
> (I’) lambda x x
> (K’) lambda y lambda x y
> (S’) lambda x lambda y lambda z (x z)(y z)
> If one looks at the typing of these
> combinators, one finds the following
> new axioms. We can call this the
> system A2, it is made up of (A),
> (M), (I), (K) and (S):
> (I) A->A
> (K) B->(A->B)
> (S) (A->(B->C))->((A->B)->(A->C))
> The rule (M) is not analytic, it introduces
> a new formula A. It can be eliminated
> similiar to forming a normal form
> of a lambda expression. A normal form
> term will either the form:
> (x r_1 .. r_n) or
> (lambda x r)
> Where r_1, .., r_n, r are again in
> normal form. A further analysis reveals
> that we can replace (M) by the following
> rule (R) which is now analytic:
> (R) G1 |- A1 &
> ..
> & Gn |- An =>
> G1 u .. u Gn u A1->..An->B |- B
> Thus another axiom set would be A3,
> consiting of (I), (D) and (R).
Thank you all for your replies
It gives me lots to think about
(although at the moment i don’t understand half of it)
But that is maybe because i am an newby in mathematical logic.
I just found it odd that most books start with explaining classical
logic and then have a sentence like:
forget DNE (Double negation elimination) and add EFQ (ex falso
quidlibed) then you have intuistic logic. (this is rephrased from P
Tomassi, logic, page 125)
It would be much better if you first start with intuistic logic and
only after that then add DNE for getting classic logic.
(I am not even sure of you really have to include EFQ as axiom, i don’t
think it is).
Intuistic logic is only a bit more diffucult but much more a proof
theory then classical logic.
In article <1158186438.989474.105…@i3g2000cwc.googlegroups.com>,
- Hide quoted text — Show quoted text -
"transl…@googlemail.com" <transl…@googlemail.com> wrote:
> Thank you all for your replies
> It gives me lots to think about
> (although at the moment i don’t understand half of it)
> But that is maybe because i am an newby in mathematical logic.
> I just found it odd that most books start with explaining classical
> logic and then have a sentence like:
> forget DNE (Double negation elimination) and add EFQ (ex falso
> quidlibed) then you have intuistic logic. (this is rephrased from P
> Tomassi, logic, page 125)
> It would be much better if you first start with intuistic logic and
> only after that then add DNE for getting classic logic.
> (I am not even sure of you really have to include EFQ as axiom, i don’t
> think it is).
Without EFQ you cannot intuitionistically prove
A v B, ~A |- B
> Intuistic logic is only a bit more diffucult but much more a proof
> theory then classical logic.
Eh?
transl…@googlemail.com wrote:
> I just found it odd that most books start with explaining classical
> logic and then have a sentence like:
> forget DNE (Double negation elimination) and add EFQ (ex falso
> quidlibed) then you have intuistic logic. (this is rephrased from P
> Tomassi, logic, page 125)
> It would be much better if you first start with intuistic logic and
> only after that then add DNE for getting classic logic.
Yeah, one is a sublogic of the other, but that doesn’t mean you should
start with the sublogic first. Otherwise, where do you draw the line?
Do you want to start with the most "minimal" logic and then build your
way up the infinite ladder to….That’s right, you’d never reach an
interesting logic in your life time!
> > It would be much better if you first start with intuitionistic logic and
> > only after that then add DNE for getting classic logic.
> Yeah, one is a sublogic of the other, but that doesn’t mean you should
> start with the sublogic first.
Two quick comments on this thread. First, it’s much more natural —
isn’t it?? — to think in terms of a natural deduction system for
intuitionistic logic (rather than an axiomatically presented system).
And second, there is *some* rationale for thinking that classical logic
is (so to speak) intuitionistic logic plus an add-on which requires
independent defence, rather than thinking of inituitionistic logic as a
hobbled version of classical logic. For suppose you think that the
introduction rules give the meaning of the connectives, and then the
defensible elimination rules are those which are in harmony with the
introduction rules. Then that naturally(!) generates intuitionistic
logic, but doesn’t give us a defence of DNE, which then needs some
independent justification.
Michael Dummett and Neil Tennant have writted extensively on this sort
of theme.
- Hide quoted text — Show quoted text -
Barb Knox wrote:
> In article <1158186438.989474.105…@i3g2000cwc.googlegroups.com>,
> "transl…@googlemail.com" <transl…@googlemail.com> wrote:
> > Thank you all for your replies
> > It gives me lots to think about
> > (although at the moment i don’t understand half of it)
> > But that is maybe because i am an newby in mathematical logic.
> > I just found it odd that most books start with explaining classical
> > logic and then have a sentence like:
> > forget DNE (Double negation elimination) and add EFQ (ex falso
> > quidlibed) then you have intuistic logic. (this is rephrased from P
> > Tomassi, logic, page 125)
> > It would be much better if you first start with intuistic logic and
> > only after that then add DNE for getting classic logic.
> > (I am not even sure of you really have to include EFQ as axiom, i don’t
> > think it is).
> Without EFQ you cannot intuitionistically prove
> A v B, ~A |- B
Why should you want to prove that in the first place?
I am not sure but i thought you can prove
A v B, ~A |- ~~ B
without EFQ.
And is this not reintruducing the Law of the excluded middle in a
roundabout way?
A, ~A |- ~~B
> > Intuistic logic is only a bit more diffucult but much more a proof
> > theory then classical logic.
> Eh?
Missing RAA makes it a bit more difficult
I am still stuck in proving
P -> (Q & ~Q) : ~P
without using RAA
transl…@googlemail.com wrote:
> Missing RAA makes it a bit more difficult
> I am still stuck in proving
> P -> (Q & ~Q) : ~P
> without using RAA
Hold on! Intuitionistic logic allows RAA in the form
P
…
C & not-C
________
not-P
It’s the following which isn’t intuitionistically acceptable
not-P
…
C & not-C
________
P
- Hide quoted text — Show quoted text -
mordov wrote:
> transl…@googlemail.com wrote:
> > I just found it odd that most books start with explaining classical
> > logic and then have a sentence like:
> > forget DNE (Double negation elimination) and add EFQ (ex falso
> > quidlibed) then you have intuistic logic. (this is rephrased from P
> > Tomassi, logic, page 125)
> > It would be much better if you first start with intuistic logic and
> > only after that then add DNE for getting classic logic.
> Yeah, one is a sublogic of the other, but that doesn’t mean you should
> start with the sublogic first. Otherwise, where do you draw the line?
> Do you want to start with the most "minimal" logic and then build your
> way up the infinite ladder to….That’s right, you’d never reach an
> interesting logic in your life time!
Interesting with many sublogics excist before "standard" positive
minimal logic
(intuistic logic without MT?)
i only come to
Pure implication logic (no negation only -> )
Implication logic with negation added
And and implication logic ( with & and ~ (ok the name is not proper)
full implication logic with & and ~ and v (ok the name is not proper)
This with MT equals Intuistic logic (without EFQ)
Other strands positive logic (-> & and v but no ~)
wich (sub)logics, am i missing?
Or should the list be completely different? By naming rules of
inference oid)
I find it more interesting each day.
You are right but I find RAA a derived rule not a primitive one.
And i am still struggling to prove it.
I have the opinion that MT (modus tollens) is primitiverule
And RAA (of witch there seem to be two forms) a derived one
The two forms:
RAA 1 P -> ~P : ~P
RAA 2 P -> (Q & ~Q) : ~P
I have proven RAA 1 but RAA2 is to difficult for me
- Hide quoted text — Show quoted text -
Peter_Smith wrote:
> transl…@googlemail.com wrote:
> > Missing RAA makes it a bit more difficult
> > I am still stuck in proving
> > P -> (Q & ~Q) : ~P
> > without using RAA
> Hold on! Intuitionistic logic allows RAA in the form
> P
> …
> C & not-C
> ________
> not-P
> It’s the following which isn’t intuitionistically acceptable
> not-P
> …
> C & not-C
> ________
> P
transl…@googlemail.com says…
>wich (sub)logics, am i missing?
Well, one of the most limited logics is "linear logic" invented
by Girard:
http://en.wikipedia.org/wiki/Linear_logic
–
Daryl McCullough
Ithaca, NY
"transl…@googlemail.com" wrote:
> I just found it odd that most books start with explaining classical
> logic
Presumably that’s because they are books on classical logic. Read a
book on intuitionistic logic such as the one I mentioned.
–
Remove "antispam" and ".invalid" for e-mail address.