Minimal logic valid?
Jan Burse
~A, ~A->(B->A) |- ~B
MoeBlee
> ~A, ~A->(B->A) |- ~B
I don't know what the semantics are for minimal logic, so I don't know
about validity in minimal logic, but why wouldn't the proof I gave in
the other thread (about the above being intuitionistically valid) show
that ~B is derivable from {~A, ~A -> (B -> A)} in minimal logic?
In that proof I didn't use anything not permitted by intuitionistic
logic and I didn't use ex falso quodlibet. (Isn't minimal logic
intuitionistic logic without ex falso quodlibet?)
1. ~A ... premise {1}
2. ~A -> (B -> A) ... premise {2}
3. B -> A .... modus ponens 1, 2 {1 2}
4. B ... supposition {4}
5. A ... modus ponens 3, 4 {1 2 4}
6. ~B ... by contradiction 1, 4, 5 {1 2}
MoeBlee
Jan Burse
Ex contradictione implies ex falso, look see:
Ex contracdictione: EC:(A->f)->(A->B)
Ex falso: EF:f->B
------ (Id)
f |- f
--------- (-> right) ------------------- EC
|- f -> f |- (f->f) -> (f->B)
--------------------------------------------- (MP)
|- f -> B
So minimal logic cannot have EC, as we have already
stated that it does not have EF.
So your prove will not go through in this way
in minimal logic.
Bye
MoeBlee
> MoeBlee schrieb:
> > 1. ~A ... premise {1}
> > 2. ~A -> (B -> A) ... premise {2}
> > 3. B -> A .... modus ponens 1, 2 {1 2}
> > 4. B ... supposition {4}
> > 5. A ... modus ponens 3, 4 {1 2 4}
> > 6. ~B ... by contradiction 1, 4, 5 {1 2}
> Ex contradictione implies ex falso, look see:
>
> Ex contracdictione: EC:(A->f)->(A->B)
I didn't use that.
I used: (A -> f ) -> ~A.
MoeBlee
MoeBlee
Actually, in context of the argument, it was 'B' not 'A'
(B -> f) -> ~B
MoeBlee
Jan Burse
>
> ~A, ~A->(B->A) |- ~B
>
And what about?
|- exists x forall y (p x y) -> forall y exists x (p x y)
Derivable in minimal logic?
Bye
William Elliot
What's minimal logic?
Frederick Williams
I know what it is in the propositional case:
http://home.utah.edu/~nahaj/logic/structures/systems/johansson.html but
what the quantifier rules/axioms are I don't know.
--
Remove "antispam" and ".invalid" for e-mail address.
Jan Burse
> William Elliot wrote:
>> On Sat, 7 Jun 2008, Jan Burse wrote:
>>
>>> Jan Burse schrieb:
>>>> ~A, ~A->(B->A) |- ~B
>>> And what about?
>>>
>>> |- exists x forall y (p x y) -> forall y exists x (p x y)
>>>
>>> Derivable in minimal logic?
>>>
>> What's minimal logic?
>
> I know what it is in the propositional case:
> http://home.utah.edu/~nahaj/logic/structures/systems/johansson.html but
> what the quantifier rules/axioms are I don't know.
>
http://users.rsise.anu.edu.au/~jks/minlog.html
But I can give you condensed propositional
and quantifier case:
------- (Id)
A |- A
G |- A
----------- (|- ->)
G\B |- B->A
G |- A H |- A -> B
--------------------- (MP)
GuH |- B
G |- A
---------------(forall intro) x not free in G
G |- forall x A
G |- forall x A
---------------
G |- A[x/t]
Defs: ~A := A->f, exists x A := ~forall x~A.
translogi
I think there is no real agreed definition what minimal logic really
is
I do remember seeing two different incompatible versions of it.
(one containing negation the other without it)
The problem is that Johansons article on minimal logic (that is
somewhere available on the internet) leans heavenly on a paper from
Heyting that is well known but hardly read. ( It is German, it is old
(1936?) and It isn't available on the internet, I sometimes do wonder
if people who refer to it actually have seen it.) I do have a copy of
it somewhere. (I literaly had to go to the British library to make a
copy of it)
It really is a shame that Heytings article isn't available online and
in english.
As far as i can remember out of my head
Johanssons minimal logic has negation
But even Johanson makes an alternative with a constand false version
EFQ (ex falso Quidlibet ) does not hold
But (p & ~p) -> ~q does
With f being falsehood
p & ~p just means
p & (p -> f)
So by modus ponens
f
q -> f is just a weakening of this
and
~q is just shorthand for q- > f
translogi
Just found Johanssons paper
http://archive.numdam.org/ARCHIVE/CM/CM_1937__4_/CM_1937__4__119_0/CM_1937__4__119_0.pdf
Yes is in German as well
the axioms for Fol minimal logic are
AxFx -> fx
and
Fx -> ExFx
(page 6 of this article)
Johanson makes the remark on page 3 (freely translated)
"This work is not independent readable, the reader should have the
works of Heyting and Gentzen which are widely available within reach,
so that it is unnessesary to copy from these works.",
the references are to Heyting's
Die formalen regeln der Intuitionistischen logic 1930
and Gentzen.s
Untersuchungen uber das logische schlieszen (sa 1935?)
Heytings work is even older than I thought
Jan Burse
> Johanson makes the remark on page 3 (freely translated)
>
> "This work is not independent readable, the reader should have the
> works of Heyting and Gentzen which are widely available within reach,
> so that it is unnessesary to copy from these works.",
>
> the references are to Heyting's
> Die formalen regeln der Intuitionistischen logic 1930
> and Gentzen.s
> Untersuchungen uber das logische schlieszen (sa 1935?)
>
> Heytings work is even older than I thought
I am not refering to Johanssons for the definition of
minimal logic.
Probably Johanssons uses the term minimal logic
in a different sense than this term is nowadays used.
Nowadays we can indentify natural deduction
calculi NM, NJ and NK:
NM: Minimal logic, no rule for "bottom"
NJ: Intuitionistic logic
NK: Classical logic
See for example:
http://www-ls.informatik.uni-tuebingen.de/psh/lehre/ss08/bwfl/nk-ni-nm.pdf
William Elliot
> Frederick Williams schrieb:
>> William Elliot wrote:
>>> On Sat, 7 Jun 2008, Jan Burse wrote:
>>>
>>>> Jan Burse schrieb:
>>>>> ~A, ~A->(B->A) |- ~B
>>>> And what about?
>>>>
>>>> |- exists x forall y (p x y) -> forall y exists x (p x y)
>>>>
>>>> Derivable in minimal logic?
Isn't this also called natural deduction?
Yes, I think so.
forall y, pxy -> pxy -> exists x, pxy
exists x forall y, pxy -> exists x exists x, pxy -> exists x, pxy
exists x forall y, pxy -> forall y exists x forall y, pxy
-> for all y exists x, pxy
What do yuu think?
Jan Burse
> Isn't this also called natural deduction?
>
> Yes, I think so.
>
> forall y, pxy -> pxy -> exists x, pxy
> exists x forall y, pxy -> exists x exists x, pxy -> exists x, pxy
> exists x forall y, pxy -> forall y exists x forall y, pxy
> -> for all y exists x, pxy
>
> What do yuu think?
>
I having problems to understand your posting,
could you please place a little bit more parenthesis
and explanation!
But I think you are using "left existential introduction"
in your first step, isn't it?
I think this is not derivable in minimal logic,
when we have only:
exists x A(x) :<=> forall x (A(x) -> f) -> f
Bye
Jan Burse
>
> ~A, ~A->(B->A) |- ~B
>
Is "left existential introduction"
derivable in NM (minimal logic):
|- forall x(A(x) -> B) -> (exists x A(x) -> B), ~(x fr B)
I believe not. Think we would need
double negation elimination.
Bye
Note: Minimal logic does only have
forall and ->, and only rules for these.
~A := A -> f
exists x A(x) := ~ forall x ~ A(x)
Neither |- f -> A, nor |- ~~A -> A holds
in minimal logic.
William Elliot
> William Elliot schrieb:
>
>> Isn't this also called natural deduction?
>>
>> Yes, I think so.
forall y (pxy) -> (pxy) -> exists x (pxy)
exists x forall y (pxy) -> exists x exists x (pxy) -> exists x (pxy)
exists x forall y (pxy) -> forall y exists x forall y (pxy)
-> for all y exists x (pxy)
>> What do yuu think?
> I having problems to understand your posting,
> could you please place a little bit more parenthesis
Ok, I'm having some problem with your over clipping.
For example, what is that we're suppose to be proving?
> and explanation!
>
p -> q -> r is common short hand for (p -> q)&(q -> r).
> But I think you are using "left existential introduction"
> in your first step, isn't it?
>
What's wrong with that? Purely natural, is it not.
> I think this is not derivable in minimal logic,
> when we have only:
>
> exists x A(x) :<=> forall x (A(x) -> f) -> f
I dispute that using that definition is natural logic.
Why not define
forall x (px)
as
(exists x (px -> f)) -> f ?
Those definitions aren't intuitionistic nor constructive.
Why does exist x (px) mean what it's supposed to mean?
If it does, then by the same reasoning forall x (px)
as defined means what it's supposed to mean.
However those two definitions are not equivalent in natural logic.
Hence by preferring one over the other, the symmetry or duality
of 'forall' and 'exists' is discarded.
Natural logic consequently uses separate axioms or introduction,
elimination rules for each connective. For example. Which is preferable?
p&q for ~p v ~q or p v q for ~p & ~q?
With -> as primitive, what's p & q? ~(p -> q) ?
Ok, prove the naturally intuitive
p & q -> p
Assume p & q.
Assume p -> f
Thus p -> q (using f -> q).
Hence f.
Consequently ~~p.
p & q -> ~~p
Bash. Nothing natural about that and for
being minimal, it gets complicated quickly.
For example, what can you do with the simple '&' problem without
using f -> q ?
Jan Burse
> ... a lot of pondering on "natural" ...
No, minimal logic, is not supposed to be
natural, although it has a natural STYLE
deduction system. Its only the style that is
adopted, not the stance.
You can imagine minimal logic as metamath
without the following rule axiom:
|- (~A -> ~B) -> (B -> A)
And here you go, you have a hilbert STYLE
deduction system. We could also adopt that
style, but we will not import the whole
hilbert program right now.
And question is not whether minimal logic
is natural or hilbertian or what ever,
but what it can derive.
Best Regards
translogi
I do agree there seems to be a different sense about what minimal
logic is.
But i still, think the terms comes from Johanson so the reference i
gave is then the "founding document"
And I guess it is the first time term NM for natural deduction for
minimal logic is used.
Johanson does mention natural deduction "naturlichen schlieszens" ($5
pag16) and NM is defined there as the
calculi in which the following deduction (25 in Gentzens work)
_|_
--------
D
is removed.
Johannsons writes just after this
" Analog to the names NJ (Natural Intuitionistic) and NK (Natural
Classical) We will call this calculi NM (Natural Minimal) "
I haven't read Gentzens work,where Johansons refers to , I am not sure
it is available on line or in a library
I do see some small problems if there is no _|_ elimnation rule
How do you go from
b v (a & ~a )
to
b
?
Johansons does describe that it is a problem (number 7 on page 9) and
gives later a "meta-logical" proof of this as a valid deduction but i
cannot follow him here.
(It uses two differend kinds of sequent calculi, then i got lost)
Strangly in Hilbert style Minimal logic it is (b v (a & ~a)) -> b is
NOT a theorem
(see page 6 4.41)
Ps notice that in Johannons truth tables
0 stands for true
and
1 stands for false
(if you want to compare them with present day truthtables)
Greetings
Jan Burse
> Strangly in Hilbert style Minimal logic it is (b v (a & ~a)) -> b is
> NOT a theorem
> (see page 6 4.41)
>
> Ps notice that in Johannons truth tables
> 0 stands for true
> and
> 1 stands for false
> (if you want to compare them with present day truthtables)
>
> Greetings
>
In my minimal logic, I dont have v or &.
Its minimal implication logic.
So thats the name I should use.
Also in minimal implication logic, defining
v and & on top of ->, with the semantic, as
it tends to have in intuitionistic implication
logic, is not likely possible. Maybe this
is what Johannson shows?
Except if you have second order variant of it,
see other thread about this. Then minimal
implication logic is what Sorensen &
Urzyczyin call the "simplified syntax", and
its possible to define intuitionistic logic
in it.
Bye
translogi
Are you talking about minimal logic or about ICI?
System ICI (Intuitionist Calculus of Implication)
see
http://home.utah.edu/~nahaj/logic/structures/systems/ici.html
That is a very basic implication only logic.
only 2 short axioms
p -> (q->p)
(p->(q->r)) -> ((p->q)->(p->r))
(BTW (((p->q)->p)->p) Peirce's law is not a theorem in this system
(It is also invalid in Minimal and Intuitionistic logic)
you can add the rules axioms for &, v and <--> without any
disturbance
(p -> (q -> (p&q)) & I
(p & q ) -> p &E
(p & q ) -> q &E
p -> (p v q) vI
q -> (p v q) vI
(p->r) ->((q->r) -> ((p v q) ->r)) vE
( p -> q) -> ((q -> p) -> (p <--> q)) <--> I
(p <--> q) -> (p -> q) <-->E
(p <--> q) -> (q -> p) <-->E
this all together is
PPL
http://home.utah.edu/~nahaj/logic/structures/systems/ppl.html
The problems starts when you add negation in one way (~) or another (_|
_)
What are the rules for them?
That is where the logics go their own way
Clasical (~a -> _|_) -> a
Intuitionistic _|_ -> a
Minimal am not sure anymore, maybe something like _|_ is just
shorthand for (x & ~x) a kind of parameter
Do you have negation in a form of ~ or _|_ ?
if so, what rules do you have for them.
(No rules just means that _|_ is a variable it can even be true)
That is the real problem.
greetings
Jan Burse
> Do you have negation in a form of ~ or _|_ ?
> if so, what rules do you have for them.
> (No rules just means that _|_ is a variable it can even be true)
> That is the real problem.
>
> greetings
>
Repeating my posting from 2008-06-07, I have:
------- (Id)
A |- A
G |- A
----------- (|- ->)
G\B |- B->A
G |- A H |- A -> B
--------------------- (MP)
GuH |- B
G |- A
---------------(forall intro) x not free in G
G |- forall x A
G |- forall x A
--------------- (forall elim)
G |- A[x/t]
Only five rules dealing with -> and forall.
A constant f, but no rules about it.
Negation define as shorthand: ~A := A->f
But no explicit rule for negation.
Nevertheless some laws about negation are derivable,
for example:
|- A-> ((A->f)->f)
Is derivable, here is a derivation:
---------------(id) ------ (id)
A-> f |- A -> f A |- A
----------------------------- (MP)
A-f, A |- f
----------------- (|- ->)
A |- (A->f) -> f
----------------- (|- ->)
|- A->((A->f)->f)
Or when using the shorthand ~A, we have equally:
---------------(id) ------ (id)
~A |- ~A A |- A
----------------------------- (MP)
~A, A |- f
----------------- (|- ->)
A |- ~~A
----------------- (|- ->)
|- A -> ~~A
The five rules (MP), (id), (|- ->), (Inst)
and (Gen) are NM.
As can be seen double negation introduction
can be derived in NM.
When we add:
---------
|- f -> A
We get NJ (Intuitionistic).
When we add (to NM) :
-----------
|- ~~A -> A
We get NK (Classical).
MoeBlee
> Jan Burse schrieb:
> > ~A, ~A->(B->A) |- ~B
That's holds in minimal logic, as I showed.
> And what about?
>
> |- exists x forall y (p x y) -> forall y exists x (p x y)
>
> Derivable in minimal logic?
Why wouldn't it be?
1 ExAy Pxy ... premise
2 Ay Pxy ... EI
3 Pxy ... UI
4 Ex Pxy ... EG
5 AyEx Pxy ... UI
P.S. Unless stated otherwise, I take the following as a deductive
system for minimal logic (and any derived rules, including a natural
deduction system thus derived):
If P, Q, and R are formulas, and t is a term, and v is a variable,
then
Inference rule: From P and P -> Q, infer Q.
Axioms: All closures of:
P -> (Q -> P)
(P -> (Q -> R)) -> ((P -> Q) -> (P -> R))
P -> (Q -> (P & Q))
(P & Q) -> P
(P & Q) -> Q
P -> (P v Q)
P -> (Q v P)
(P -> Q) -> ((R -> Q) -> ((P v R) -> Q))
(P -> Q) -> ((P -> ~Q) -> ~P))
AvP -> P[t|v] (if t is free for v in P)
P[t|v] -> EvP (if t is free for v in P)
(P -> Q) -> (P -> AvQ) (if v does not occur free in Q)
(P -> Q) -> (EvP -> Q) (if v does not occur free in Q)
/
Intuitionistic logic is acheived by adding
~P -> (P -> Q)
/
Classical logic is acheived by adding
~P -> (P -> Q)
P v ~P
~Ax~P -> ExP
MoeBlee
Jan Burse
> On Jun 6, 6:21 pm, Jan Burse <janbu...@fastmail.fm> wrote:
>> Jan Burse schrieb:
>
>>> ~A, ~A->(B->A) |- ~B
>
> That's holds in minimal logic, as I showed.
>
>> And what about?
>>
>> |- exists x forall y (p x y) -> forall y exists x (p x y)
>>
>> Derivable in minimal logic?
>
> Why wouldn't it be?
>
> 1 ExAy Pxy ... premise
> 2 Ay Pxy ... EI
> 3 Pxy ... UI
> 4 Ex Pxy ... EG
> 5 AyEx Pxy ... UI
>
> P.S. Unless stated otherwise, I take the following as a deductive
> system for minimal logic (and any derived rules, including a natural
> deduction system thus derived):
> (P -> Q) -> (EvP -> Q) (if v does not occur free in Q)
The minimal implicational logic based on -> and
A, cannot derive:
(P -> Q) -> (EvP -> Q), v not in Q
Provided that E is defined as ~A~.
The problem is that minimal implicational logic
cannot derive:
~~P -> P
If it could, it would be classical. So its
easy to find a proof of:
(P -> Q) -> (~Av~P -> ~~Q), v not in Q
But I dont see that this is further sharpened
to the following:
(P -> Q) -> (~Av~P -> Q)
As long as the above is not derivable in
my minimal implicational logic, I dont
think that your system without ~A->(A->B)
is the same as my minimal implicational logic.
Bye
MoeBlee
> The minimal implicational logic based on -> and
> A, cannot derive:
>
> (P -> Q) -> (EvP -> Q), v not in Q
>
> Provided that E is defined as ~A~.
And indeed, just as in intuitionistic logic, E is not defined as ~A~.
I intentionally did not list such a definition or equivalence.
> I dont
> think that your system without ~A->(A->B)
> is the same as my minimal implicational logic.
It might not be the same as your minimal implicational logic. But it
is the minimal logic I found in the textbook 'Propositional Logics' by
Epstein (though the quantifier axioms I used are just from
intuitionistic logic), said there to be based on Johansson 1936, and
also from another source that I don't recall right now. By the way,
the Epstein book gives Fitting's variation on Kripke semantics for the
(propositional) system, an alternative equivalent axiomatization in
which f is primitive instead of ~, and an outline of a completeness
proof.
That is, these sources take minimal logic to be exactly intutionisitic
logic except witthout ex falso quodlibet, just as I have.
MoeBlee
Jan Burse
> That is, these sources take minimal logic to be exactly intutionisitic
> logic except witthout ex falso quodlibet, just as I have.
>
> MoeBlee
And then you get all the anomalies of admissible but
not derivable rules...
http://en.wikipedia.org/wiki/Admissible_rule
See Kreisel–Putnam rule
I am not so sure, but I think my minimal implicational
logic does not have these defects.
Or does it?
From the Wiki Page:
Intuitionistic logic itself is not structurally complete, but
its fragments may behave differently. Namely, any
disjunction-free rule or implication-free rule
admissible in a superintuitionistic logic is derivable.
If it would say "subintuitionistic", instead of
"superintutionistic", then my claim about structural
completness would be confirmed.
Bye
MoeBlee
>
> > That is, these sources take minimal logic to be exactly intutionisitic
> > logic except witthout ex falso quodlibet, just as I have.
> And then you get all the anomalies of admissible but
> not derivable rules...
I don't know. The distinction between admissable and derivable is not
one I've studied. Looks interesting though. I'm going to make a note
to learn more about it.
But if you wouldn't mind, would you explain why it would be considered
a problem for a rule to be admissable but not derivable. What does it
hurt?
MoeBlee
Jan Burse
> But if you wouldn't mind, would you explain why it would be considered
> a problem for a rule to be admissable but not derivable. What does it
> hurt?
>
> MoeBlee
Purity. Then there somehow two systems around:
- Meta logic of admissibility
- Logic of derivability
If the logic is not structurally complete,
you cannot find A / B, by simply asking
|- A -> B.
Bye
Jan Burse
This is quite interesting:
http://www.iphils.uj.edu.pl/rml/rml-38/dzik.pdf
He takes:
H : negation free fragment of intuitionistic predicate logic
Lin : (A -> B) v (B -> A)
Well: (A -> exists x B) -> exists x(A -> B)
LW := H+Lin+Well
He claims that LW is hereditarily structurally
complete, whereas H, H+Lin and H+Well are
not structurally complete.
MoeBlee
What is 'A / B' and what do you mean by "asking" |- A -> B?
MoeBlee
Jan Burse
A / B : When |- A then |- B mathematically observed,
A / B is called an *admissible* rule.
|- A -> B : |- = turnstile = derivability in minimal
implicational logic, means A -> B is *derivable*.
Clearly |- A -> B implies A / B, but do we also
have A / B implies |- A -> B?
BTW: Here is a proof that |- A -> B implies A / B.
Assume |- A -> B and |- A, then by MP rule:
|- A -> B |- A
--------------------
|- B
Hence also |- B is derivable. Hence A / B.
MoeBlee
> A / B : When |- A then |- B mathematically observed,
> A / B is called an *admissible* rule.
I'm trying to figure out that Wikipedia article. You're leaving out
the part about substitution functions.
And what is the definition of "mathematically observed"?
MoeBlee
translogi
I am going a bit back to an older post
This is NOT natural deduction, you are using
This is sequent calculus (schluszweisenkalkul), something different
all together
I am not a regular user of this kind of calculus
But i do remember that there are some restrictions when using it for
intuitionistic logic.
(I thought restrictions on the -> A role)
Am not sure if you have the right restrictions when you are using it
for minimal logic.
Johansson does refer to it but by lack on where he refers to (Gentzens
work) I don't know the restrictions for minimal logic.
(it mentions that the rules NES and NEA need to be replaced with
different rules.)
see page [16] 133
I was puzzeling with minimal logic realised that
(P & ~P) <-> (Q & ~Q) is NOT a theorem in minimal logic (but is in
intuitionistic logic)
For minimal logic
(P & ~P) -> _|_ is a theorem
_|_ -> (P & ~P) is NOT a theorem
_|_ -> ~P is a theorem
_|_ is in Johansson "/\" "Widerspruch","a contradiction" or "etwas
Falsches" "some falsehood"
NOT "all falshoods"
(what would be a good translation of "_|_" in intuitionistic or
classical logic)
also
((P -> Q) & (P-> ~Q)) -> ~P is a theorem in minimal logic
(It is an axiom (4.11) in Heytings version of intuitionistic logic.
And is the only axiom about negation in Johansson
I am not sure about the remark on the
KreiselPutnam rule:
(~P -> (Q v R)) -> ((~P -> Q) v (~P -> R))
I don't think you can derive it using intuitionistic natural
deduction.
Minimal logic is subintuitionistic I do agree with that.
found a paper about admissable rules
http://math.cas.cz/~jerabek/papers/indep.pdf
Greetings
Jan Burse
> This is NOT natural deduction, you are using
> This is sequent calculus (schluszweisenkalkul), something different
> all together
You see the text of gentzen is very easy to
obtain. You can find it here:
http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17178
Gentzen introduces two calculi:
NJ, NK: "Natürliches Schliessen"
= translates to "Natural Deduction"
LJ, LK: "Schlussweisen Kalküle"
= translates to Sequent Calculus"
I will now show you that my calculus is among NJ, NK
and not among LJ, LK.
The only difference between Gentzens presentation
and my presentation is that Gentzen uses a graphic
representation with detachment indicated specially.
Whereas I am using a more flat representation.
That both representations amount to the same system
is a well known fact, and there are even papers about
it. Its even part of the results of Gentzens original
paper itself.
I will try to give a rough intuitive explanation
why both representation yield the same system.
We have the following graphic rules:
(Page 186 of the above paper)
[A] A A -> B
B ---------
------ B
A -> B
These graphics rules are steps in a proof tree.
The [A] indicates that this A is a detached
assumption. So when something is a detached
assumption, it will only temporarily used,
and then later in the proof tree not anymore
referenced (the position of it).
What my flat representation makes explicit,
is what can be referenced, what is available
as an assumption. In my flat representation
we have the following corresponding rules:
G |- B G |- A D |- A -> B
------------- ---------------------- ---------
G\A |- A -> B GuD |- B A |- A
This is in accordance with what Gentzen about
the transition from NJ, NK to LJ, LK:
(Page 190 of the above paper, towards the bottom)
"Das naheliegendste Verfahren, um aus einer NJ
Herleitung eine logistische Herleitung zu machen,
ist dieses: Man ersetzt eine H Formel B
welche avon den Annahmeformeln A1,..,An abhängt
durch die neue Formel A1,..,An |- B."
So when a formula B depends on the assumption A1,..,An
in the graphic representation, then we write for
it A1,..,An |- B.
So my system is natural deduction.
Jan Burse
> So when a formula B depends on the assumption A1,..,An
> in the graphic representation, then we write for
> it A1,..,An |- B.
>
> So my system is natural deduction.
BTW: This belongs also to gentzen:
http://gdz.sub.uni-goettingen.de/no_cache/dms/load/img/?IDDOC=17188
To complete my claim, we must pick an LJ, LK
derivation and show that it is not NJ, NK.
This is easy for LK, because it allows
sequents of the form
A1,..,An |- B1,..,Bn
Which we do not have in NJ, NK, when n<>1.
But LJ is supposed to have n=1.
So we must look at the inference steps in
LJ. For LJ the cut looks as follows:
G |- A A, D |- B
------------------
G, D |- B
We dont find such a rule in Gentzen. Why?
Is this not a natural rule? Can we not depict
it graphical? Is it really not part of NJ?
Pah, its could be also part of NJ:
D |- B
--------
G |- A D\A |- A-> B
---------------------------
GuD\A |- B
So the graphical representation is:
[A]
A B
-------------
B
So a broader view, hopefully shared today,
is that natural deduction is single
sukzedent sequent calculus.
But what does Gentzen do in his part II
paper. He even goes back to hilbert
style deductions.
Another beast, which can be seen as
zero antezedent and single sukzedent
sequent calculus.
Think the poor guy (Gentzen) needed
something to write about.
Bye
Alan Smaill
> So a broader view, hopefully shared today,
> is that natural deduction is single
> sukzedent sequent calculus.
The usual view, going back to Gentzen, is that intuitionistic sequent
calculus is the single succedent version of classical sequent
calculus.
> But what does Gentzen do in his part II
> paper. He even goes back to hilbert
> style deductions.
>
> Another beast, which can be seen as
> zero antezedent and single sukzedent
> sequent calculus.
>
> Think the poor guy (Gentzen) needed
> something to write about.
>
> Bye
--
Alan Smaill
Jan Burse
> The usual view, going back to Gentzen, is that intuitionistic sequent
> calculus is the single succedent version of classical sequent
> calculus.
There are also classical sequent calculi possible
with single sukzedent. Gentzen was probably a little
bit to dramatic in this point.
Here is a classical implicational single
sukzedent calculus:
------
A |- A
G |- A D |- A -> B
---------------------
GuD |- B
G |- B
-------------
G\A |- A -> B
----------------- (double negation elimination)
|- ((A->f)->f)->A
Give me any classical implicational tautology,
which is not derivable in the above calculus.
You wont find one. Please try.
And its single sukzedent. Its the mininal
implicational calculus plus a single rule
for negation:
NK = NM + (double negation elimination).
See my Schroeder Heister reference in another post.
Best Regards
Jan Burse
> I was puzzeling with minimal logic realised that
> (P & ~P) <-> (Q & ~Q) is NOT a theorem in minimal logic (but is in
> intuitionistic logic)
> _|_ -> (P & ~P) is NOT a theorem
Duno, I dont use &. Would need to recast it with
implication, if possible.
> _|_ -> ~P is a theorem
Yes. f->(P->f) is a theorem. Its an
instance of lets call it (Weakening):
A |- A
--------- (|- ->)
A |- B->A
------------ (|- ->)
|- A->(B->A)
|- ->: Right implication introduction.
(Also known as K in combinatorial logic)
> ((P -> Q) & (P-> ~Q)) -> ~P is a theorem in minimal logic
I would rather have a look at:
((P -> ~Q) & (P-> Q)) -> ~P
Here the translation to implicational logic is
a little bit easier.
(P->(Q->f))->((P->Q)->(P->f))
Yes its a theorem. Its an instance
of lets call it (Distribution):
1: A->(B->C) |- A->(B->C)
2: A |- A
3: A->(B->C), A |- B->C (MP 1, 2)
4: A->B |- A->B
5: A |- A
6: A->B, A |- B (MP 4, 5)
7: A->(B->C), A->B, A |- C (MP 3, 6)
8: A->(B->C), A->B |- A->C (|- -> 7)
9: A->(B->C) |- (A->B)->(A->C) (|- -> 8)
10: |- (A->(B->C))->((A->B)->(A->C)) (|- -> 8)
(Also known as S in combinatorial logic)
> http://math.cas.cz/~jerabek/papers/indep.pdf
Hm
translogi
Thanks for the links to Gentzens works.
I didn't mean that your way was invalid
But it surely looks more like sequent calculus than natural deduction.
even the reference you gave
This is in accordance with what Gentzen about
the transition from NJ, NK to LJ, LK:
(Page 190 of the above paper, towards the bottom)
"Das naheliegendste Verfahren, um aus einer NJ
Herleitung eine logistische Herleitung zu machen,
ist dieses: Man ersetzt eine H Formel B
welche avon den Annahmeformeln A1,..,An abhängt
durch die neue Formel A1,..,An |- B."
is in the part where Gentzen explains sequent calculus.
(schluszweisenkalkule)
I just thought the |- that you use was equal to the ---> arrow in
sequent calculus. (wikipedia, http://en.wikipedia.org/wiki/Sequent_calculus
even uses |- for the arrow)
In natural deduction there is only ->
I do not say that Natural deduction and the sequent calculi for the
same logic give different results. If that were the case something
would be wrong.
But sequent calculi (LJ LK) is just something else than natural
deduction.(NJ NK)
(In my humble opinion)
I prefer the Lemmon style natural deduction, but it is all mostly a
mater of taste i guess.
Greetings
Jan Burse
> I do not say that Natural deduction and the sequent calculi for the
> same logic give different results. If that were the case something
> would be wrong.
> But sequent calculi (LJ LK) is just something else than natural
> deduction.(NJ NK)
> (In my humble opinion)
Like a gaisha is not same as a farmers daughter.
My rules are the same as in:
http://planetx.cc.vt.edu/AsteroidMeta/Natural_deduction_based_metamath_system
The turnstile has the following meaning:
$c |- $. $( read 'the following sequence is provable from the previous
list of hypotheses (called a context)' $)
Here is my axiom id:
$( The only axiom of the natural deduction. $)
ax-hyp $a # [ G , ph ] |- ph $.
Here is essentially my rule |- ->:
${
ax-ii.1 $e # [ G , ph ] |- ps $.
$( Implication introduction. It is the deduction theorem that is
embedded here. In the context of a Hilbert system this theorem is
a meta theorem. In the context of natural deduction it is an axiom. $)
ax-ii $a # G |- ( ph -> ps ) $.
$}
Here is essentially my rule MP:
${
ax-ie.1 $e # G |- ph $.
ax-ie.2 $e # G |- ( ph -> ps ) $.
$( Implication elimination. $)
ax-ie $a # G |- ps $.
$}
Everything runs under the heading "natural deduction",
the G |- A, is the operationalization of natural deduction.
The graphical presentation can not be put into the
computer. What we can put into the computer is these
G |- As.
The link contains much more rules, because in my
rules I have for contexts: GuD the composition
of contexts and D\A the detachment from a context.
The many more rules cater for that.
And there are many more rules for /\, \/, Abs.
Abs = f. But the implicational fragment should
be ->.
The following rule makes it NJ:
${
axin.1 $e # G |- Abs $.
$( To have an intuitionistic propositional + predicate calculus
system ax-cl should be replaced by axin. The other axioms
should remain untouched. However to work with an intuitionistic
system you will have to be cautious. Not all the definitions
traditional in a classic system are allowed. For instance
we could not have defined ' E. x ph 'as ' -. A. x -. ph '. $)
axin $p # G |- ph $=
( wabs wn ax-we ax-cl ) ABADBECFG $.
$( [?] $) $( [15-Oct-05] $)
$}
The rule is:
G |- f
------ (axin)
G |- A
I rather prefer only to introduce:
--------- (ex falso quodlibet)
|- f -> A
Via MP we get the same:
---------- (ex falso quodlibet)
G |- f |- f -> A
--------------------- (MP)
G |- A
And vice versa:
------- (Id)
f |- f
------- (axin)
f |- A
-------- (|- ->)
|- f -> A
There are many hints in the above. First that exists x A is
not the same as ~forall x~ A in NJ. And that axin is
derivable from ax-cl.
The following rule makes it NK:
${
ax-cl.1 $e # [ G , -. ph ] |- Abs $.
$( contra ( classical logic ). See axin for intuitionistic logic. $)
ax-cl $a # G |- ph $.
$}
This is not the same as I was proposing. The
above amounts to:
G, A->f |- f
--------------
G |- A
I was proposing:
-------------------- (~~elim)
|- ((A->f)->f) -> A
But they are interderivable again:
G, A->f |- f
-------------- (|- ->) -------------------- (~~elim)
G |- (A->f)->f |- ((A->f)->f) -> A
------------------------------------------ (MP)
G |- A
And:
---------------------- (id) ------------ (id)
(A->f)->f |- (A->f)->f A->f |- A->f
--------------------------------------------- (MP)
(A->f)->f, A->f, |- f
---------------------
(A->f)->f |- A
---------------
|- ((A->f)->f) -> A
Citing the author of nat.mm:
Natural deduction was invented by Gentzen in the 30's (cf. Gentzen,
Untersuchungen uber das logische Schliessen (Mathematische Zeitschrift
39, pp. 176-210, 405-431 1934-5)). His aim was to give a logic system
where propositional and predicate calculus proofs would be easier to
make than in previously designed systems (cf. for example D.Hilbert,
W.Ackermann. Grundzuge der theoretischen Logik. Berlin (Springer),
1928).
To achieve this goal Gentzen uses a list of hypotheses (called
context in this file).
Our system is not exactly the system designed by Gentzen but it can be
considered as a descendant of it. A descendant of the Hilbert
system is obviously the system described by Norman Megill in set.mm
To understand exactly how Gentzen derived his own system from the
Hilbert's system I recommend the reading of ` Introduction to
metamathematics ` by Kleene chapter V (In fact I'm not sure in
this chapter Kleene tries to derive Gentzen's system from Hilbert's one
but it can really be read that way.
Question of the day: Why is it a decedant?
Answer: Gentzen uses another rule to make NK from NM.
Namely, he uses |- A v ~A.
Remark: The difference is not in the graphical representation
or the use of sings like --> versus |-. This would be too
trivial.
Bye
Jan Burse
> Jan Burse <janb...@fastmail.fm> writes:
>
>> So a broader view, hopefully shared today,
>> is that natural deduction is single
>> sukzedent sequent calculus.
>
> The usual view, going back to Gentzen, is that intuitionistic sequent
> calculus is the single succedent version of classical sequent
> calculus.
>
Ebbinghaus and Flum have a single succedent
calculus, for classical logic.
Even Modus Ponens is not a rule in their
system, but a derived rule.
The derive it from contradiction and
proof by cases.
Bye
Alan Smaill
> Alan Smaill schrieb:
> > Jan Burse <janb...@fastmail.fm> writes:
> >
> >> So a broader view, hopefully shared today,
> >> is that natural deduction is single
> >> sukzedent sequent calculus.
> > The usual view, going back to Gentzen, is that intuitionistic sequent
> > calculus is the single succedent version of classical sequent
> > calculus.
> >
>
> Ebbinghaus and Flum have a single succedent
> calculus, for classical logic.
Of course, it can be done.
But Gentzen's observation is that we can get intuitionistic
sequent calculus by a simple restriction on the shape of the
sequents used classically; and thst is more than a syntactic
coincidence in my view.
> Even Modus Ponens is not a rule in their
> system, but a derived rule.
>
> The derive it from contradiction and
> proof by cases.
This rather suggests that single succedent sequent calculus
does not correspond to natural deduction ...
> Bye
--
Alan Smaill
Jan Burse
>> The derive it from contradiction and
>> proof by cases.
>
> This rather suggests that single succedent sequent calculus
> does not correspond to natural deduction ...
Yes, and 2+2=4 indicates that 4 belongs not
to peano arithmetic, as it is derived and not
builtin.
Bye
Alan Smaill
I agree that wasn't a convincing suggestion --
but there is a serious point to be made here, however ...
You did suggest that single succedent sequent calculus corresponds to
natural deduction, yet the most natural system obtained from classical
sequent calculus under that restriction is still a sequent calculus
system (for intuitionist logic). Pointing out the existence of a
single succedent sequent calculi for classical logic was
not convincing on your part either.
I welcome arguments to the contrary.
> Bye
--
Alan Smaill
Jan Burse
> You did suggest that single succedent sequent calculus corresponds to
> natural deduction, yet the most natural system obtained from classical
There is something to multi sukzedent calculi and classicality.
Because to be able to move things in multiple to the left side,
needs some form of negation:
G, ~A |- D
----------
G |- A, D
So in a minimal logic, which has no double negation elimination
we will have problems in pursuing a multi sequent calculi.
But because multi sukzedent calculi allow classicality, but do
not allow non classical logic, does not imply that single
sukzedent calculi are not ammeneable to classical logic.
You are subject to the simple fallacy of uniqueness of
examples:
P(a) -> forall x(P(x) -> x=a)
P(x) : calculus x can do classical logic
a : multi sukzedent calculi
You can replace P also by "can do classical logic naturally",
"can do classical logic ....", put your favorite adjective
"..." here.
How do you measure these adjectives, natural, etc.. They are
not logical notions. But to be a little scientifc you need
measurable conditions.
If you give me a classical multi sequent calculus, I will
give you a corresponding natural deduction style calculus,
with the same order of proof depth.
The reason is that we instead of a rule:
G |- A, B
----------
G |- A v B
We could also use a rule:
G, ~A |- B
----------
G |- A v B
BECAUSE we are classical. And we will thus stay as a natural
deduction style calculus. And guess the proofs will have
the same shape.
Bye
Alan Smaill
> Alan Smaill schrieb:
> > You did suggest that single succedent sequent calculus corresponds to
> > natural deduction, yet the most natural system obtained from classical
>
> There is something to multi sukzedent calculi and classicality.
> Because to be able to move things in multiple to the left side,
> needs some form of negation:
>
> G, ~A |- D
> ----------
> G |- A, D
>
> So in a minimal logic, which has no double negation elimination
> we will have problems in pursuing a multi sequent calculi.
>
> But because multi sukzedent calculi allow classicality, but do
> not allow non classical logic, does not imply that single
> sukzedent calculi are not ammeneable to classical logic.
I agree to that (and have already agreed this point earlier
in the thread).
> You are subject to the simple fallacy of uniqueness of
> examples:
>
> P(a) -> forall x(P(x) -> x=a)
>
> P(x) : calculus x can do classical logic
> a : multi sukzedent calculi
>
> You can replace P also by "can do classical logic naturally",
> "can do classical logic ....", put your favorite adjective
> "..." here.
>
> How do you measure these adjectives, natural, etc.. They are
> not logical notions. But to be a little scientifc you need
> measurable conditions.
More scientifically, I note that it is the case in most
constructive logics that a proof of some x.P(x) yields
a term in the language such that P(t) is provable;
in corresponding classical cases this is not the case.
> If you give me a classical multi sequent calculus, I will
> give you a corresponding natural deduction style calculus,
> with the same order of proof depth.
>
> The reason is that we instead of a rule:
>
> G |- A, B
> ----------
> G |- A v B
>
> We could also use a rule:
>
> G, ~A |- B
> ----------
> G |- A v B
>
> BECAUSE we are classical. And we will thus stay as a natural
> deduction style calculus. And guess the proofs will have
> the same shape.
I find this unsatisfactory as an argument, because the proof system
you end up with loses a basic property of sequent calculi which
makes them well suited for proof search, as Gentzen already noted,
namely producing analytic proofs -- proofs where all the formulas
appearing in the proof are subformulas of the original formula.
The notion of analytic proof is scientific.
Do you find anything in the comparison between Gentzen's
sequent and ND calculi for intuitionist logic that suggests
another, more scientific, criterion for distinguishing
between the ND and sequent formulations? From what you have said
so far, there seems no grounds for making a distinction ND/sequent
in this case at all. For me, the discharging of hypotheses
in the ND case is what makes the difference.
> Bye
--
Alan Smaill
Jan Burse
> More scientifically, I note that it is the case in most
> constructive logics that a proof of some x.P(x) yields
> a term in the language such that P(t) is provable;
> in corresponding classical cases this is not the case.
A similar note can be made for classical logic. Namely
if we have :
T |- exists x A(x)
Then there are some t_1,..,t_n, such that:
T |- A(t_1) v .. v A(t_n)
In some constructive logic we have always n=1, in
classical logic in the general case we cannot
assume that n=1 will hold.
Here is a simple classical example:
p(a) v p(b) |- exists x p(a)
p(a) v p(b) |/- p(a)
p(a) v p(b) |/- p(b)
p(a) v p(b) |- p(a) v p(b)
But although this note is scientifical, it is
not tied to proofs. You dont make a statement
about a proof object. You make a statement about
the implication from a valid statement to another
valid statement.
So the above lemma with the t_1,..,t_n holds
independent what calculus you use. Whether you
use NK or LK, or whatever. It doesnt give you a
property of a calculus.
And the lemma with n=1 holds independentent
what calculus you use. Whether you us Nx or
Lx, or whatever. It doesnt give you a property
of a calculus.
>> If you give me a classical multi sequent calculus, I will
>> give you a corresponding natural deduction style calculus,
>> with the same order of proof depth.
>>
>> The reason is that we instead of a rule:
>>
>> G |- A, B
>> ----------
>> G |- A v B
>>
>> We could also use a rule:
>>
>> G, ~A |- B
>> ----------
>> G |- A v B
>>
>> BECAUSE we are classical. And we will thus stay as a natural
>> deduction style calculus. And guess the proofs will have
>> the same shape.
> I find this unsatisfactory as an argument, because the proof system
> you end up with loses a basic property of sequent calculi which
> makes them well suited for proof search, as Gentzen already noted,
> namely producing analytic proofs -- proofs where all the formulas
> appearing in the proof are subformulas of the original formula.
> The notion of analytic proof is scientific.
No, the single sukzedent calculus for classical logic will also
produce analytic proofs. It will also have the sub formula
property, eventually prefixed by a negation sign. But this
is enough to be analytical. Calculi are analytical when the
do not force someone in backward search, to invent a formula.
For example modus ponens is not analytical:
A A -> B
-------------- (MP)
B
It forces you to invent A to prove B. There are analytical
calculi for classical and non classical logic. Its not a
domain of classical logic. Gentzen himself shows with LJ
an analytical calculus for a non classical logic.
But value of analytical proofs is very much dimished by the
fact that a proof might force someone to invent terms.
So this is the real show stopper for analytical proofs
when quantifiers are around, that you need to invent terms.
But you are right, "analyticality" is a property of proofs,
and not a property between valid statements. So you are
on the right track.
> Do you find anything in the comparison between Gentzen's
> sequent and ND calculi for intuitionist logic that suggests
> another, more scientific, criterion for distinguishing
> between the ND and sequent formulations? From what you have said
> so far, there seems no grounds for making a distinction ND/sequent
> in this case at all. For me, the discharging of hypotheses
> in the ND case is what makes the difference.
For me "natural deduction" is an idiomatic phrase, and
it would never ever come to my mind to search some
meaning in it that is related to a notion of "natural".
What makes "natural numbers" natural?
And the paper by Gentzen implies to me, that "natural
deduction" is categorized as "single sukzedent" "sequent
calculus". "single sukzedent" is the least property
for me so that something falls into the category
of "natural deduction".
What concerns "discharging", because it is available
in "sequent calculus", it is also available in "natural
deduction". That the context changes it shape by losing
formulas is not an exclusive property of "natural deduction".
This regularly also happens in multi sukzedent calculi.
Still awaiting a better definition of "natural" from you.
translogi
>
> - Show quoted text -
Natural deduction is just the name of a proof method that Gentzen
developed.
It is called natural because it is "close" to he perceived that humans
reason.
It got this name in contrast with axiomatic reasonings a la Hilbert
Russelll ect.
I do see that here the term natural deduction is used for Sequent
calculi and i do disagree with that.
The main difference is that natural deduction uses lots of inference
rules and no axioms.
while the axiomatic method uses axioms(chemata) and only detachment /
modus ponens
There are many styles of natural deduction
I do prefer natural deduction in the style of Lemmon Pospesel Thomassi
ed.
(see for example logic primer by Allan and Hand)
Maybe Human / intelligent reasoning would have been a better name in
the first place, but it just was not given that name.
Greetings
Jan Burse
> The main difference is that natural deduction uses lots of inference
> rules and no axioms.
> while the axiomatic method uses axioms(chemata) and only detachment /
> modus ponens
Hilbert style calculi usually have no detachment rule.
Natural deduction has it. What are you talking
about?
In natural deduction you have a context G, and
you can formulate a rule as such:
G |- A
-----------
G\B |- B->A
Or graphically:
[B]
A
-----
B -> A
Hilbert style calculi dont have this context.
They have just rules over a single sukzedent
sequents with zero context.
But a hilbert style calculi might make use
of axioms G, and then we write also:
G |- A
And we might have the meta result, that when
G |- A is valid, that G\B |- B->A is also
valid. That is called the deduction theorem.
The deduction theorem states that when there
is a hilbert style proof G |- A, then
there is "another" hilbert style proof of
G\B |- B->A.
That hilbert style methods need more axiom schemas,
I agree. Namely to be classical, because things
go rather into the axioms than into the rules.
But that hilbert style is an axiomatic method,
while natural deduction is not, I wouldn't
agree. For example as soon as one has the
classical apparatus in both system, one can
work the same way with axiom systems.
Also an axiom schema is a degenerated instance
of the following pattern of a rule:
Template_1 .... Template_n
--------------------------
Template
An axiom schema has just n=0, i.e. no precluding
patterns. So we can compare hilbert style and
natural deductions:
System Templateform n
---------------------------------------------
Hilbert style |- A =0 for the logic axioms
=0 for the axioms
=2 for MP
Natural deduction G |- A =1, 2, 3 for the logic rules
=0 for axioms and assumptions
=1 for detachment
=2 for MP
I think both systems belong to the axiomatic method
as there are some principles (the rules with n=0
or n<>0) layed down, and we try to work from these
principles.
Bye
translogi
Hilbert style proof that p ->p
This is the simplest proof of something 'obvious', It can get much
worse
axioms
C1 (p->(q->p))
C2 ((p->(q->r))->((p->q) -> (p->r)))
rules
Detachment
given (or proved) A->B and A B is proved
substitution
any variable may be replaced by any other variable or formula.
(But all variables need to be replaced)
Theorem D1 is axiom C2 with p replaced by r
((p->(q->p))->((p->q) -> (p->p)))
Theorem D2 is the detachment from theorem D1 given axiom C1
((p->q) -> (p->p)))
Theorem D3 is theorem D2 with q replaced with (q->p)
((p->(q-> p)) -> (p->p)))
Theorem D4 is the detachment from D1 given C1
(p->p)))
Probably more in line with Hilberts thinking is:
Theorem E1 is axiom C2 with
p replaced by r
q replaced by (q->p)
E1 = ((p->((q->p)->p))->((p->(q->p)) -> (p->p))))
Theorem E2 is axiom C1 with
q replaced by (q->p)
E2 = (p->((q->p)->p))
E3 is the detachment from theorem E1 given theorem E2
E3 = ((p->(q->p)) -> (p->p)))
E4 is the detachment from theorem E3 given axiom C1
E4 = (p -> p)
You can from these two axioms and rules prove
(p->((p->q) ->p))
((p -> q) -> ((q->r) -> (p->r)))
((p->(q->r)) -> (q->(p->r)))
and so on
But it is hard work (as shown above)
in lemmon style natural deductiom
in lemmon style natural deductiom
1 1 p Assumption
- 2 p-> p 1,1 ->I
is just so much more easier.
although proving
((p->(q->r))->((p->q) -> (p->r)))
is done this way
1 1 (p->(q->r) A
2 2 (p-q) A
3 3 p A
2,3 4 q 2,3 ->E
1,3 5 (q->r) 1,3 ->E
1,2,3 6 r 4,5 ->E
1,2 7 (p->r) 3-6 ->I
1 8 ((p->q) -> (p->r)) 2-7 ->I
- 9 ((p->(q->r))->((p->q) -> (p->r))) 1-8 ->I
.
Jan Burse
> rules
> Detachment
> given (or proved) A->B and A B is proved
What you are calling "detachment",
is MP (Modus Ponens) and not (-> intro).
> Hilbert style proof that p ->p
yep
> Lemmon style proof of p->p
yes its shorter.
> Lemmon style proof of a hilbert style axiom
yes its interderivable.
BTW: What did you want us to tell?
translogi
I wanted to show how they are different.
In working
in getting to a conclusion.
Was thinking of doing the axiomatic method in Polish notation
then logic really just becomes manipulation of (meaningless) strings
In axiomatic circles it is called detachment
modus ponens is the theorem (p -> ((p->q) ->q)
(CpCCpqq in Polish notation)
Also i wanted to promote the Lemmon style of natural deduction
much easier to understand than tree structures
Greetings
Was planning to write how to proof modus ponens but it is just to
complicated
see
http://www.clas.ufl.edu/users/jzeman/modallogic/chapter01.htm
and
http://www.clas.ufl.edu/users/jzeman/modallogic/chapter02.htm
(this uses a slightly more complicated form of detachment is a bit
pushing substitution and detachment in one operator but it is well
explained in chapter 1)
and yes it is all in polish notation
modus ponens is no 2.16
Jan Burse
> modus ponens is the theorem (p -> ((p->q) ->q)
>
> (CpCCpqq in Polish notation)
Summary of our new notation gobbling:
- Lemmon style: Natural deduction style, but
instead of a tree, lines and reference numbers.
- Polish Notation: Formulas instead with infix
notation, with prefix notation
We can possibly enlarge this list of variantions
ad infinitum. Here are some more:
- Fitch style (*): Like lemmon style, but we can
eliminate repeating the context on each line.
Instead that each line looks like:
...
G |- A
We simply write:
...
A
This works for a great deal of natural deduction
style rules, except for abstraction:
...
G |- A
-------------
G\B |- B -> A
So in case of having this rule in a proof, we simply
use a new notational concept, namely we change the
indent.
B
| ..
| A
B -> A
Right? (Stil little bit redundant for abstraction, but
other non-minimal logic rules might profit a little
bit more, than just the minimal logic rules)
- Reverse Polish Notation(**): Formulas instead with infix
notation, with suffix notation. So instead Cpq, we
write pqC for p->q.
What else? Peirce alpha-graphs?
Bye
(*) http://en.wikipedia.org/wiki/Fitch-style_calculus
(**) http://en.wikipedia.org/wiki/Reverse_Polish_Notation
Balthasar
wrote:
>>
>> ~A, ~A->(B->A) |- ~B
>>
> [...] why wouldn't the proof I gave in the other thread (about the
> above being intuitionistically valid) show that ~B is derivable from
> {~A, ~A -> (B -> A)} in minimal logic?
>
> In that proof I didn't use anything not permitted by intuitionistic
> logic and I didn't use ex falso quodlibet. (Isn't minimal logic
> intuitionistic logic without ex falso quodlibet?)
>
It is (if I'm right).
>
> 1. ~A ... premise {1}
> 2. ~A -> (B -> A) ... premise {2}
> 3. B -> A .... modus ponens 1, 2 {1 2}
> 4. B ... supposition {4}
> 5. A ... modus ponens 3, 4 {1 2 4}
> 6. ~B ... by contradiction 1, 4, 5 {1 2}
>
Right. Or
1 (1) ~A A
2 (2) ~A -> (B -> A) A
1,2 (3) B -> A 1,2 ->E
4 (4) B A
1,2,4 (5) A 3,4 ->E
1,2,4 (6) A & ~A 1,5 &I
1,2 (7) ~B 4,6 ~I
B.
--
"For every line of Cantor's list it is true that this line does not
contain the diagonal number. Nevertheless the diagonal number may
be in the infinite list." (WM, sci.logic)
Balthasar
wrote:
>
> Ex contradictione [quodlibet] implies ex falso [quodlibet], look see:
>
> Ex contracdictione [quodlibet]: EC[Q]: (A->f)->(A->B)
> Ex falso: EF[Q]: f->B
>
>
> ------ (Id)
> f |- f
> --------- (-> right) ----------------------- EC[Q]
> |- f -> f |- (f -> f) -> (f -> B)
> ------------------------------------------------- (MP)
> |- f -> B
>
> So minimal logic cannot have EC[Q], as we have already
> stated that it does not have EF[Q].
>
Right.
>
> So your prove will not go through in this way
> in minimal logic.
>
He did not use ECQ in his proof.
Jan Burse
(~A = A -> f, and refraining from &)
Balthasar
wrote:
>>>>
>>>> ~A, ~A->(B->A) |- ~B
>>>>
>>> [...] why wouldn't the proof I gave in the other thread (about the
>>> above being intuitionistically valid) show that ~B is derivable from
>>> {~A, ~A -> (B -> A)} in minimal logic?
>>>
>>> In that proof I didn't use anything not permitted by intuitionistic
>>> logic and I didn't use ex falso quodlibet. (Isn't minimal logic
>>> intuitionistic logic without ex falso quodlibet?)
>>>
>> It is (if I'm right).
>>
>> [...]
>>
>>
> How about not using & and ~ in your proof?
> (~A = A -> f, and refraining from &)
Variant 1, NM (with ~ as a primitive):
1 (1) ~A A
2 (2) ~A -> (B -> A) A
1,2 (3) B -> A 1,2 ->E
4 (4) B A
1,2,4 (5) A 3,4 ->E
1,2,4 (6) f 1,5 ~E
1,2 (7) ~B 4,6 ~I
(The rules used above are due to Gentzen, see his systems NK, NJ.)
Variant 2, NM' (with ~ defined):
1 (1) ~A A
2 (2) ~A -> (B -> A) A
1,2 (3) B -> A 1,2 ->E
4 (4) B A
1,2,4 (5) A 3,4 ->E
1 (6) A -> f 1 def ~
1,2,4 (7) f 5,6 ->E
1,2 (8) B -> f 4,7 ->I
1,2 (9) ~B 8 def ~
Balthasar
wrote:
>>
>> I dont think that your system without ~A->(A->B)
>> is the same as my minimal implicational logic.
>>
> It might not be the same as your minimal implicational logic. But it
> is the minimal logic I found in the textbook 'Propositional Logics' by
> Epstein (though the quantifier axioms I used are just from
> intuitionistic logic), said there to be based on Johansson 1936, and
> also from another source that I don't recall right now. By the way,
> the Epstein book gives Fitting's variation on Kripke semantics for the
> (propositional) system, an alternative equivalent axiomatization in
> which f is primitive instead of ~, and an outline of a completeness
> proof.
>
> That is, these sources take minimal logic to be exactly intutionisitic
> logic except without ex falso quodlibet, just as I have.
>
Right.
"§5. Wir wollen jetzt nach dem Vorbild von G. Gentzen einen Kalkül des
natürlichen Schließens und einen Schlußweisenkalkül (Sequenzkalkül)
aufstellen und nachher deren Äquivalenz mit unserem Minimalkalkül
beweisen. Es ist dann das einfachste, daß wir von den entsprechenden
intuitionistischen Kalkülen ausgehen und bloß die darin vorzunehmenden
Änderungen angeben:
In dem Kalkül des natürlichen Schließens hat man nur das Schlußschema
_|_
---
D
wegzulassen. In Analogie mit den Bezeichnungen NJ (natürlich-
intuitionistisch) und NK (natürlich-klassisch) wollen wir den so
definierten Kalkül NM (natürlich-minimal) nennen. Gleichzeitig
betrachten wir ~A als Abkürzung für A -> _|_. (Die Möglichkeit hiervon
hat übrigens auch Gentzen selbst erkannt.)"
(Ingebrigt Johansson, Der Minimalkalkül, ein reduzierter
intuitionistischer Formalismus, 1937)
[§5. Following the lead of G. Gentzen we will formulate now a calculus
of natural deduction and a sequence calculus, and afterwards prove their
equivalence with our minimal calculus. It is simplest then that we start
of from the pertinent intuitionistic calculi and just state the
necessary changes therein:
In the calculus of natural deduction one just (only) has to omit the
schema of deduction
_|_
---
D.
In analogy with the terms NJ (natural intuitionistic) and NK (natural
classic) we want to denote the calculus defined in this way NM (natural
minimal). At the same time we consider ~A to be an abbreviation for A ->
_|_. (This possibility has already been seen by Gentzen, btw.)]
[Ingebrigt Johansson, The minimal calculus, a reduced intuitionistic
formalism, 1937]
Balthasar
wrote:
>
> Note: Minimal logic does only have
> forall and ->, and only rules for these.
>
> ~A := A -> f
> exists x A(x) := ~ forall x ~ A(x)
>
In the system of minimal logic *I* know, Ex is not defined as ~Ax~ but
taken as primitive.
_|_
---
D
_|_
---
D.
Another source, referring to Johansson's minimal calculus as /minimal
logic/ (M) is Dag Prawitz (1965, 1971).
>
> Neither |- f -> A, nor |- ~~A -> A holds
> in minimal logic.
>
Right.
Balthasar
wrote:
>
> exists x A := ~forall x~A.
>
Not so in Johansson's minimal calculus, generally referred to as as
/minimal logic/. (See Dag Prawitz [1965, 1971] for example.)
Balthasar
wrote:
>
> I am not refering to Johanssons for the definition of
> minimal logic.
>
But, imho you should. After all HE introduced that system.
>
> Probably Johanssons uses the term minimal logic
> in a different sense than this term is nowadays used.
>
No. He used it exactly the way it is used nowadays.
_|_
---
D
_|_
---
D.
>
> Nowadays we can identify natural deduction
> calculi NM, NJ and NK:
>
> NM: Minimal logic, no rule for "bottom"
> NJ: Intuitionistic logic
> NK: Classical logic
>
"In analogy with the terms NJ (natural intuitionistic) and NK (natural
classic) we want to denote the calculus defined in this way NM (natural
minimal)."
[Ingebrigt Johansson, The minimal calculus, a reduced intuitionistic
formalism, 1937]
>
> See for example:
> http://www-ls.informatik.uni-tuebingen.de/psh/lehre/ss08/bwfl/nk-ni-nm.pdf
>
Right.
Quote:
_|_
"NI (intuitionistisch) hat die Regel --- (_|_) anstelle von (_|_)c.
A
In NM (minimal) fehlt (_|_)c ersatzlos."
[NI (intuitionistisch) has the rules ... instead of (_|_)c. In NM
(minimal) there's no (_|_)c, without any replacment for it.]
Balthasar
wrote:
>
> In my minimal logic, I don't have v or &.
> It's /minimal implication logic/.
> So that's the name I should use.
>
Agree. Otherwise confusion is unavoidable.
>
> Also in minimal implication logic, defining
> v and & on top of ->, with the semantic, as
> it tends to have in intuitionistic implication
> logic, is not likely possible. Maybe this
> is what Johannson shows?
>
I guess this was achieved (for intuitionistic logic) by J. C. C.
McKinsey: "Proof of the independece of the primitive symbols of
Heyting's calculus of propositions." (1939)
http://www.jstor.org/pss/2268715
Balthasar
wrote:
>
> exists x A := ~forall x~A.
>
Not so in Johansson's minimal calculus, generally referred to as
/minimal logic/. (See Dag Prawitz [1965, 1971] for example.)
Balthasar
wrote:
>
> what about?
>
> |- ExAyP(x,y) -> AyExP(x,y)
>
> Derivable in minimal logic?
>
Sure.
1 (1) ExAyP(x,y) A
2 (2) AyP(a,y) A
2 (3) P(a,b) 2 UE
2 (4) ExP(x,b) 3 EI
2 (5) AyExP(x,y) 4 UI
1 (6) AyExP(x,y) 1,2,5 EE
(7) ExAyP(x,y) -> AyExP(x,y) 1,6 ->I
Balthasar
wrote:
>
> Is "left existential introduction" derivable in NM (minimal logic):
>
> |- Ax(P(x) -> Q) -> (ExP(x) -> Q),
>
> where x does not occure in Q.
>
Sure.
1 (1) Ax(P(x) -> Q) A
2 (2) ExP(x) A
3 (3) P(a) A
1 (4) P(a) -> Q 1 UE
1,3 (5) Q 3,4 ->E
1,2 (6) Q 2,3,5 EE
1 (7) ExP(x) -> Q 2,6 ->I
(8) Ax(P(x) -> Q) -> (ExP(x) -> Q) 1,7 ->I
Jan Burse
Oki Doki
But your quote doesnt say whether he starts with
an implicational fragment or not. I.e. whether he
includes &, v in his considerations or not.
Bye
Jan Burse
> On Sun, 08 Jun 2008 07:56:52 +0200, Jan Burse <janb...@fastmail.fm>
> wrote:
>
>> Is "left existential introduction" derivable in NM (minimal logic):
>>
>> |- Ax(P(x) -> Q) -> (ExP(x) -> Q),
>>
>> where x does not occure in Q.
>>
>
> Sure.
>
> 1 (1) Ax(P(x) -> Q) A
> 2 (2) ExP(x) A
> 3 (3) P(a) A
> 1 (4) P(a) -> Q 1 UE
> 1,3 (5) Q 3,4 ->E
> 1,2 (6) Q 2,3,5 EE
> 1 (7) ExP(x) -> Q 2,6 ->I
> (8) Ax(P(x) -> Q) -> (ExP(x) -> Q) 1,7 ->I
>
>
> B.
>
>
and no v, &). So only rules for Ax, but no rules for Ex.
Is then "left existential introduction" still derivable
in NM?
In particular do we have?
|-NM forall x(A -> B) -> ((~ (forall x (~ A))) -> B)
when x does not occur in B
I doubt.
Bye
Balthasar
wrote:
>>
>> [§5. Following the lead of G. Gentzen we will formulate now a calculus
>> of natural deduction and a sequence calculus, and afterwards prove their
>> equivalence with our minimal calculus. It is simplest then that we start
>> of from the pertinent intuitionistic calculi and just state the
>> necessary changes therein:
>>
>> In the calculus of natural deduction one just (only) has to omit the
>> schema of deduction
>>
>> _|_
>> ---
>> D.
>>
>> In analogy with the terms NJ (natural intuitionistic) and NK (natural
>> classic) we want to denote the calculus defined in this way NM (natural
>> minimal). At the same time we consider ~A to be an abbreviation for A ->
>> _|_. (This possibility has already been seen by Gentzen, btw.)]
>>
>> [Ingebrigt Johansson, The minimal calculus, a reduced intuitionistic
>> formalism, 1937]
>
> Oki Doki
>
> But your quote doesnt say whether he starts with
> an implicational fragment or not. I.e. whether he
> includes &, v in his considerations or not.
>
Actually, it does (at least concerning it's natural deduction form).
Since in Gentzen's classical and intuitionistic calculi & and v are
treated as undefined primitives, this also holds for NM (Natural
minimal), after all the _only_ difference (modulo ~A = A -> _|_) between
NJ and NM is that the latter does not have the bottom rule. (And _of
course_ in the minimal calculus in Frege-Hilbert style &, v are treated
as undefined primitive symbols. After all, minimal logic is just "a
reduced intuitionistic formalism.")
Note that the minimal calculus is modeled on Heyting's intuitionistic
calculus: "Der Minimalkalkül unterscheidet sich von dem von Heyting
aufgestellten intuitionistischen Formalismus nur darin, daß sein
Axiom 4.1 fehlt." [The minimal calculus differs from the intuitionistic
formalism constructed by Heyting only in the omission of his axiom 4.1.]
(Ingebrigt Johansson, The minimal calculus, a reduced intuitionistic
formalism, 1937). And the latter CANNOT be set up without treating & and
v as undefined primitive symbols. (See J. C. C. McKinsey: "Proof of the
independece of the primitive symbols of Heyting's calculus of
propositions." (1939)
Jan Burse
> Note that the minimal calculus is modeled on Heyting's intuitionistic
> calculus: "Der Minimalkalkül unterscheidet sich von dem von Heyting
> aufgestellten intuitionistischen Formalismus nur darin, daß sein
> Axiom 4.1 fehlt." [The minimal calculus differs from the intuitionistic
> formalism constructed by Heyting only in the omission of his axiom 4.1.]
> (Ingebrigt Johansson, The minimal calculus, a reduced intuitionistic
> formalism, 1937). And the latter CANNOT be set up without treating & and
> v as undefined primitive symbols. (See J. C. C. McKinsey: "Proof of the
> independece of the primitive symbols of Heyting's calculus of
> propositions." (1939)
Maybe McKinseys should be revised to some decree.
& is conservative in minimal logic natural deduction.
I think we have:
If G and B do not contain & then
G |-NM(->,&) B iff G |-NM(->) B
So the & is independent yes. But its also dependent,
as we have:
A1 & .. & An |- B iff
A1, .., An |- B
G |- B1 & .. & Bn iff
G |- B1 and .. and G |- Bn
Anyway, I am not interested in & for the moment.
Bye
Balthasar
wrote:
>>>
>>> Is "left existential introduction" derivable in NM (minimal logic):
>>>
>>> |- Ax(P(x) -> Q) -> (ExP(x) -> Q),
>>>
>>> where x does not occure in Q.
>>>
>> Sure.
>>
>> 1 (1) Ax(P(x) -> Q) A
>> 2 (2) ExP(x) A
>> 3 (3) P(a) A
>> 1 (4) P(a) -> Q 1 UE
>> 1,3 (5) Q 3,4 ->E
>> 1,2 (6) Q 2,3,5 EE
>> 1 (7) ExP(x) -> Q 2,6 ->I
>> (8) Ax(P(x) -> Q) -> (ExP(x) -> Q) 1,7 ->I
>>
> What about when Ex is defined as ~Ax~ (and ~A = A -> f,
> and no v, &). So only rules for Ax, but no rules for Ex.
> Is then "left existential introduction" still derivable
> in NM?
>
I tried, but came to the same conclusion as you did; i.e. I got stuck at
|- Ax(P(x) -> Q) -> (ExP(x) -> ~~Q).
>
> In particular do we have?
>
> |-NM forall x(A -> B) -> ((~ (forall x (~ A))) -> B)
> when x does not occur in B
>
> I doubt.
>
I guess you might be right.
Balthasar
wrote:
>
> Maybe McKinseys should be revised to some decree.
>
Errr...?
>
> & is conservative in minimal logic natural deduction.
> I think we have:
>
> If G and B do not contain & then
>
> G |-NM(->,&) B iff G |-NM(->) B
>
> So the & is independent yes.
>
???
Actually, I guess "independence" (mentioned by McKinsey) here is
referring to the (im)possibility to _define_ one of the connectives with
help of the remaining connectives.
Ah right, just found a appropriate quote:
"The intuitionistic connectives are not interdefinable: none of ->, &,
v, ~ can be defined in terms of the others. Heyting had stated this in
Heyting 1930 (p. 44), but without giving a proof. A proof was published
by Wajsberg (1938) and (independently and by different methods) by
McKinsey (1939)"
Source:
http://plato.stanford.edu/entries/intuitionistic-logic-development/
Jan Burse
> Actually, I guess "independence" (mentioned by McKinsey) here is
> referring to the (im)possibility to _define_ one of the connectives with
> help of the remaining connectives.
Interdefinability seems to be a stronger requirement,
than conservative extension.
Check out:
Subintuitionistic Logics
Greg Restall
Source: Notre Dame J. Formal Logic Volume 35, Number 1 (1994), 116-129.
In the above paper BWK is minimal logic, and BWKA is
intuitionistic logic. We then find in the paper:
Theorem 4.2: L*, Lt and L*t are conservative extensions
of L, for every subintuitionsitic logic.
Sadly he does not say that fusion * collapses with &
for logics above minimal logic.
I think this result should be also found somewhere.
Bye
Balthasar
wrote:
>>
>> Actually, I guess "independence" (mentioned by McKinsey) here is
>> referring to the (im)possibility to _define_ one of the connectives
>> with help of the remaining connectives.
>>
> Check out: Greg Restall. Subintuitionistic Logics
>
You will notice that Restall also takes &, v, -> (and f) as primitive
symbols, i.e. not defined by others. As well as A and E. With other
words, there's no deviation from NJ and/or NM in this respect.
Jan Burse
> You will notice that Restall also takes &, v, -> (and f) as primitive
> symbols, i.e. not defined by others. As well as A and E. With other
> words, there's no deviation from NJ and/or NM in this respect.
>
>
> B.
>
>
> Sadly he does not say that fusion * collapses with &
> for logics above minimal logic.
> I think this result should be also found somewhere.
Will give you a reference in due time.
Bye
Jan Burse
Boolean algebras and Heyting algebras are commutative residuated
lattices in which x•y = x∧y (whence the unit I is the top element 1 of
the algebra) and both residuals x\y and y/x are the same operation,
namely implication x → y.
http://en.wikipedia.org/wiki/Residuated_lattice
Hint an enjoyable book:
RESIDUATED LATTICES: AN ALGEBRAIC GLIMPSE AT SUBSTRUCTURAL
LOGICS, 151
Nikolaos Galatos et al.
Balthasar
wrote:
>
> Hint: an enjoyable book:
> RESIDUATED LATTICES: AN ALGEBRAIC GLIMPSE AT SUBSTRUCTURAL
> LOGICS, 151
> Nikolaos Galatos et al.
>
I guess I'll take that road after having read "Logic as Algebra" by
Halmos & Givant. http://www.maa.org/reviews/logalg.html
Keith Ramsay
[...]
[quoting:]
|In the calculus of natural deduction one just (only) has to omit the
|schema of deduction
|
| _|_
| ---
| D.
If I remember correctly, if we treat intuitionistic negation
~A as an abbreviation for A->f, and then substitute some new
propositional variable for f, then the resulting formula is
derivable in intuitionistic logic if and only if the original is
derivable in minimal logic.
The double-negation interpretation from classical to
intuitionistic logic actually interprets you all the way to
minimal logic.
Keith Ramsay
Jan Burse
Nope
Alan Smaill
Jan Burse
Nope,
We have:
minimal logic
intuitionistic logic
(can be viewed as minimal logic plus axiom: f -> A)
classical logic
(can be viewed as minimal logic plus axiom: ~~A -> A)
(or alternatively as intuitionistic logic plus axiom: ~A v A)
etc..
In all of this logics, we can either work:
a) ~A is a primitive, we then need the following axiom:
(A -> B) -> ((A -> ~B) -> ~A)
b) ~A is not a primitive, but ~A := A -> f, we do not
need an axiom.
Reference (for example):
A PROPOSITIONAL CALCULUS INTERMEDIATE BETWEEN
THE MINIMAL CALCULUS AND THE CLASSICAL
CHARLES PARSONS
Notre Dame Journal of Formal Logic
Volume VII, Number 4, October 1966
Bye
Alan Smaill
> Keith Ramsay schrieb:
> > On Aug 2, 4:56 pm, Balthasar <nomail@invalid> wrote:
> > [...]
> > [quoting:]
> > |In the calculus of natural deduction one just (only) has to omit the
> > |schema of deduction
> > |
> > | _|_
> > | ---
> > | D.
> > If I remember correctly, if we treat intuitionistic negation
> > ~A as an abbreviation for A->f, and then substitute some new
> > propositional variable for f, then the resulting formula is
> > derivable in intuitionistic logic if and only if the original is
> > derivable in minimal logic.
> > The double-negation interpretation from classical to
> > intuitionistic logic actually interprets you all the way to
> > minimal logic.
> > Keith Ramsay
>
> Nope,
the following is all very well, but it doesn't contradict
Keith Ramsay's claim, as far as I can see.
> We have:
> minimal logic
> intuitionistic logic
> (can be viewed as minimal logic plus axiom: f -> A)
> classical logic
> (can be viewed as minimal logic plus axiom: ~~A -> A)
> (or alternatively as intuitionistic logic plus axiom: ~A v A)
> etc..
>
> In all of this logics, we can either work:
>
> a) ~A is a primitive, we then need the following axiom:
> (A -> B) -> ((A -> ~B) -> ~A)
>
> b) ~A is not a primitive, but ~A := A -> f, we do not
> need an axiom.
>
> Reference (for example):
>
> A PROPOSITIONAL CALCULUS INTERMEDIATE BETWEEN
> THE MINIMAL CALCULUS AND THE CLASSICAL
> CHARLES PARSONS
> Notre Dame Journal of Formal Logic
> Volume VII, Number 4, October 1966
>
> Bye
--
Alan Smaill
Jan Burse
> A PROPOSITIONAL CALCULUS INTERMEDIATE BETWEEN
> THE MINIMAL CALCULUS AND THE CLASSICAL
> CHARLES PARSONS
> Notre Dame Journal of Formal Logic
> Volume VII, Number 4, October 1966
>
> Bye
Actually trusting the source, didnt verify it by myself.
But there are many subtleties.
So it is said that when we add:
(A -> B) -> ((A -> ~B) -> ~A)
That we get a definition of negation, for any of the logics.
But watch out, if you add the following (reductio ad absurdum):
(~ A -> ~ B) -> ((~ A -> B) -> A)
Then you get classical logic.
And watch out, if you add the following (ex contradictione quodlibet):
~ A -> (A -> B)
Then you get intuitionistic logic.
Bye
Jan Burse
>>> If I remember correctly, if we treat intuitionistic negation
>>> ~A as an abbreviation for A->f, and then substitute some new
>>> propositional variable for f, then the resulting formula is
>>> derivable in intuitionistic logic if and only if the original is
>>> derivable in minimal logic.
>>> The double-negation interpretation from classical to
>>> intuitionistic logic actually interprets you all the way to
>>> minimal logic.
>>> Keith Ramsay
>> Nope,
>
> the following is all very well, but it doesn't contradict
> Keith Ramsay's claim, as far as I can see.
Ok, this is tricky.
Jan Burse
Part A
Yes follows from cut elimination. Resulting formula
does not contain f, and thus will not use the
following natural deduction rule:
G, f |- A
Thus is a proof in minimal logic, and still a proof
in minimal logic when we replace the new propositional
variable by f.
Part B
I am not interested in double negation interpretation..
Cant tell.
Bye
Balthasar
wrote:
>
> So it is said that when we add:
>
> (A -> B) -> ((A -> ~B) -> ~A) (*)
>
> That we get a definition of negation, for any of the logics.
>
> But watch out, if you add the following (reductio ad absurdum):
>
> (~A -> ~B) -> ((~A -> B) -> A) (**)
>
> Then you get classical logic.
>
> And watch out, if you add the following (ex contradictione quodlibet):
>
> ~A -> (A -> B) (***)
>
> Then you get intuitionistic logic.
>
Sure. This is well known. :-)
(*) amounts to
[A]
:
_|_
---
~A
which holds in minimal (and intuitionistic and classical) logic.
(***) amounts to
_|_
---
A
which holds in intuitionistic (and classical) logic.
and (**) amounts to
[~A]
:
_|_
-----
A
which holds in classical logic (only).
Balthasar
wrote:
>
> If I remember correctly, if we treat intuitionistic negation
> ~A as an abbreviation for A->f, and then substitute some new
> propositional variable for f, then the resulting formula is
> derivable in intuitionistic logic [I] if and only if the original is
> derivable in minimal logic [M].
>
Right. After all, in this case f does not have any special rules in M
(i.e. rules that are related to f). Hence f in M is treated like any
other propositional variable. With other words, if Phi[f] is derivable
in M, then Phi[f/B] is derivable in M, where B is some prop. variable.
Since any derivation in M is a derivation in I, this means that Phi[f/B]
can be derived in I, if Phi[f] can be derived in M. The other
"direction" of the claim is slightly more involved, I guess. At least
the following is clear: Any derivation in I which does not use the
f-rule (_|_) is a derivation in M. The idea now is: If a formula Phi,
that does not contain f, can be derived in I, it can be derived without
using the f-rule. [...] Hence if Phi[f/B] (where B is a new prop.
variable) can be derived in I, it can be derived M. And hence (by
replacing B with f throughout the derivation) Phi[f] is derivable.
[ To show: If a formula Phi, that does not contain an occurrence of f,
can be derived in I, it can be derived without using the f-rule. ]
Aatu Koskensilta
> I am not interested in double negation interpretation..
If you're not interested in the double negation interpretation why
make proclamations about it?
--
Aatu Koskensilta (aatu.kos...@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
Jan Burse
> Jan Burse <janb...@fastmail.fm> writes:
>
>> I am not interested in double negation interpretation..
>
> If you're not interested in the double negation interpretation why
> make proclamations about it?
>
Back from vacation? Nothing to do?
Bye
Aatu Koskensilta
> Back from vacation? Nothing to do?
Nothing whatsoever. Is there some reason for your continually
commenting on matters that apparently hold no interest for you or
about which you seem to know not a whit?
Jan Burse
> Jan Burse <janb...@fastmail.fm> writes:
>
>> Back from vacation? Nothing to do?
>
> Nothing whatsoever. Is there some reason for your continually
> commenting on matters that apparently hold no interest for you or
> about which you seem to know not a whit?
>
Oh it wasnt vacation. You were in prison.
No not in prison? Ok, a mental station.
Dont worry. You will get some cuddling here on sci.logic.
Including from me.
Bye
Aatu Koskensilta
> Oh it wasnt vacation. You were in prison.
>
> No not in prison? Ok, a mental station.
A mental station, indeed.
> Dont worry. You will get some cuddling here on sci.logic.
Wonderful!