iDocSlide.Com

Free Online Documents. Like!

All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.

Share

Description

In recent years a number of authors have advocated the employment of general elimination rules in the presentation of harmonious natural deduction rules for logical constants.1 Motivated by different concerns, in other publications I have given

Tags

Transcript

Inferring, splicing, and the Stoic analysis of argument
∗
Peter Milne
I
N RECENT YEARS
,
A NUMBER OF AUTHORS
, including the dedicatee of this volume, haveadvocated the employment of
general elimination rules
in the presentation of harmo-nious natural deduction rules for logical constants.
1
Motivated by different concerns, in(Milne 2008, Milne 2010) I have given natural deduction formulations of classical proposi-tional and ﬁrst-order logics employing what in (Milne 2012
b
) I call
general introduction rules
;there I show how general introduction and general elimination rules are in harmony and sat-isfy a certain inversion principle. Here I want to show how general introduction and generalelimination rules narrow, perhaps even close, the gap between Gentzen’s two ways of present-ing logic: natural deduction and sequent calculus. I shall also describe a surprisingly closeconnection with the earliest account of propositional logic that we know of, that of the Stoiclogicians. We are also led to ask after the signiﬁcance of Gentzen’s
Hauptsatz
. Until the ﬁnalsection, I shall consider only propositional logic.
1 General rules
The distinctive feature of general introduction rules is that they tell us when logically complexassumptions may be discharged; more bluntly, when they are not needed. The introducedconnective occurs as main operator in a formula occurring
hypothetically
as a logically complexassumption discharged in the application of the rule; additionally some or all of the com-ponent propositions may occur either hypothetically (as assumptions also discharged in theapplication of the rule) or categorically. In general elimination rules, by contrast, the elimi-nated connective occurs as main operator in a formula occurring
categorically
, for we are beingtold what we can draw from a logically complex proposition; some or all of the componentpropositions may occur either hypothetically (as assumptions discharged in the application of the rule) or categorically. The conclusion of either kind of rule is “general”, not determined bythe proposition containing the introduced or eliminated connective. The introduction rules forconjunction and disjunction are unexciting rewrites of standard rules; not so for negation andthe conditional, whose introduction rules are essentially classical.
∗
From Catarina Dutilh Novaes and Ole Thomassen Hjortland (eds.),
Insolubles and Consequences: Essays in Hon-our of Stephen Read
, London: College Publications, 2012, pp. 135-54.
1
See,
e.g.
, Peter Schroeder-Heister (1984
b
, 1984
a
), Neil Tennant (1992), Stephen Read (2000, 2004, 2010), SaraNegri and Jan von Plato (2001), von Plato (2001), and Nissim Francez and Roy Dyckhoff (2011).
1
conjunction
[
φ
∧
ψ
]
m
...
χ φ ψ
m
;
χφ
∧
ψ
[
φ
]
m
...
χ
m
,
χφ
∧
ψ
[
ψ
]
m
...
χ
m
.
χ
disjunction
[
φ
∨
ψ
]
m
...
χ φ
m
,
χ
[
φ
∨
ψ
]
m
...
χ ψ
m
;
χφ
∨
ψ
[
φ
]
m
...
χ
[
ψ
]
m
...
χ
m
.
χ
negation
[
¬
φ
]
m
...
χ
[
φ
]
m
...
χ
m
;
χ
¬
φ φ
.
χ
conditional
[
φ
→
ψ
]
m
...
χ
[
φ
]
m
...
χ
m
,
χ
[
φ
→
ψ
]
m
...
χ ψ
m
;
χφ
→
ψ φ
[
ψ
]
m
...
χ
m
.
χ
These rules give us a formulation of classical propositional logic with the subformula prop-erty (
cf.
Milne 2010,
§
2.7).The general form of an introduction rule is
[
(
φ
1
,
φ
2
,...,
φ
n
)]
m
...
χ
[
φ
i
1
]
m
[
φ
i
2
]
m
...
[
φ
i
k
]
m
. . ... .. . ... .. . ... .
χ χ
...
χ φ
j
1
φ
j
2
...
φ
j
l
m
-introduction
χ
where
k
+
l
≤
n
and
i
p
=
j
q
,1
≤
p
≤
k
,1
≤
q
≤
l
.The general form of an elimination rule is
(
φ
1
,
φ
2
,...,
φ
n
)[
φ
r
1
]
m
[
φ
r
2
]
m
...
[
φ
r
t
]
m
. . ... .. . ... .. . ... .
χ χ
...
χ φ
s
1
φ
s
2
...
φ
s
u
m
-elimination
χ
where
t
+
u
≤
n
and
r
p
=
s
q
,1
≤
p
≤
t
,1
≤
q
≤
u
.Given the complete set of general introduction rules for a truth-functional connective (of any
arity
), we can read off a complete set of harmonious elimination rules; we can also read off the connective’s truth-table. Likewise, given the complete set of general elimination rules fora connective, we can read off a complete set of harmonious introduction rules; we can againread off the connective’s truth-table. And given the connective’s truth-table, we can read off harmonious general introduction rules and general elimination rules. For more on why this isand ought to be the case, see (Milne 2012
b
).Derivable argument-forms yield derived inference rules. If
Σ
φ
is derivable, we canintroduce the rule2
Σ
[
φ
]
m
...
χ
m
.
χ
The converse holds trivially, for, by an application of the rule, we obtain the derivation
Σ
[
φ
]
11
.
φ
Corresponding to what is sometimes called the Rule of Assumptions—
e.g.
, in (Lemmon1965)—we have the “null rule”
φ
[
φ
]
m
...
χ
m
,
χ
which has no proper application in natural deduction proofs laid out in tree form for there
φ
counts as a proof with conclusion
φ
dependent on
φ
as assumption.
2 Splicing
We form natural deduction proof-trees by treating the conclusion of an application of one ruleastheoccurrenceofacategoricalformulaintheapplicationofanotherrule. Formulaestandingas assumptions in the application of the ﬁrst rule continue to stand as assumptions in theapplication of the second rule if not discharged (as hypothetically occurring side-premisses) inthe application of the ﬁrst. A proof of the argument-form
Σ
ψ
is a proof tree in which onlymembers of
Σ
remain as undischarged assumptions and
φ
stands as the conclusion, at the rootof the proof-tree.I want to consider a different way of manipulating rules. I call it
splicing
. Splicing is carriedout by cross-cancelling a hypothetical occurrence of a formula in one rule and a categoricaloccurrence of the same formula in another rule to obtain a new rule. Splicing is to be thoughtof as a new primitive operation acting directly on
rules in schematic form
. Employing splicing,we can ﬁnd (general) introduction and elimination rules for logically complex formulae. Forexample, exclusive disjunction can be represented as
(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)
. Splicing gives us ina succession of steps:
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
∨
ψ
¬
(
φ
∧
ψ
)
m
⊕
χ
[
φ
∨
ψ
]
m
...
χ φ
m
=
χ
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
¬
(
φ
∧
ψ
)
m
;
χ
3
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
¬
(
φ
∧
ψ
)
m
⊕
χ
[
¬
(
φ
∧
ψ
)]
m
...
χ
[
φ
∧
ψ
]
m
...
χ
m
=
χ
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
[
φ
∧
ψ
]
m
...
χ
m
;
χ
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
[
φ
∧
ψ
]
m
...
χ
m
⊕
χφ
∧
ψ
[
ψ
]
m
...
χ
m
=
χ
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
[
ψ
]
m
...
χ
m
.
χ
In similar fashion, we obtain the introduction rule
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ
[
φ
]
m
...
χ ψ
m
χ
and the elimination rules
(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)
φ ψ
and
χ
(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)[
φ
]
m
...
χ
[
ψ
]
m
...
χ
m
.
χ
Had we spliced
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
[
φ
∧
ψ
]
m
...
χ
m
χ
with the other
∧
-elimination rule,
i.e.
, with
φ
∧
ψ
[
φ
]
m
...
χ
m
,
χ
we would have obtained this rule
[(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)]
m
...
χ φ
[
φ
]
m
...
χ
m
χ
4
which, being a
weakening
of the null rule, is quite acceptable but utterly uninformative regard-ing
(
φ
∨
ψ
)
∧¬
(
φ
∧
ψ
)
. (Quite generally, if we accept a rule, we can accept any weakeningobtained by adding formulae whether that be in categorical occurrences or hypothetical.)The expressive adequacy of, say,
{¬
,
∧
,
∨}
(or, indeed any other expressively adequateset) in classical propositional logic translates into the capacity of splicing to be a techniquefor generating (sets of) general introduction and general elimination rules for arbitrary
n
-arytruth-functional connectives. By way of example, the computer programmer’s favourite,‘if
φ
then
ψ
, else
χ
’, which we shall abbreviate as ‘
(
φ
,
ψ
,
χ
)
’, is classically equivalent to
(
φ
∧
ψ
)
∨
(
¬
φ
∧
χ
)
. This is equivalent to the negation of
(
φ
∨¬
χ
)
∧
(
¬
φ
∨¬
ψ
)
. Inspection of the results of splicing in the case of exclusive disjunction shows that splicing will yield theserules:
introduction rules
[
(
φ
,
ψ
,
χ
)]
m
...
υ
[
φ
]
m
...
υ χ
m
and
υ
[
(
φ
,
ψ
,
χ
)]
m
...
υ φ ψ
m
;
υ
elimination rules
(
φ
,
ψ
,
χ
)
φ
[
ψ
]
m
...
υ
m
and
υ
(
φ
,
ψ
,
χ
)[
φ
]
m
...
υ
[
χ
]
m
...
υ
m
.
υ
(
φ
,
ψ
,
χ
)
is also equivalent to
(
φ
→
ψ
)
∧
(
¬
φ
→
χ
)
. Splicing, starting with this formula,gets us the very same rules.
2.1 Algebra ...or maybe not
With splicing and other operations that we may perform on rules, we have a certain amountof structure.Splicing is not a function: while in any application of splicing there is only one formulacancelled, a hypothetical occurrence in one rule being crossed off against a categorical occur-rence in the other, there may be more than one formula available for cancellation. So, strictlyspeaking, questions of associativity and commutativity do not arise. Instances of the null ruledo act as
identity elements
in that,
when we can splice
, splicing with an instance of the null ruleyields the srcinal rule (and there can’t be any question about which formula is up for can-cellation unless the other rule involved is already an instance of the null rule or a weakeningthereof). (Recall that in order to splice two rules, the same formula must occur hypotheticallyin one rule and categorically in the other, hence the qualiﬁcation ‘when we can splice’.)Counting every rule as a weakening of itself, there is an uninteresting partial orderinggiven by the relation
rule X is a weakening of rule Y
.The negation rules play a special role: splicing an introduction rule with the instance of thenegation elimination rule containing the introduced formula yields an elimination rule for theintroduced formula’s negation. Conversely, splicing an elimination rule with the instance of 5

We Need Your Support

Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks