An
axiomatization of the set of valid formulas of the
full language of Section 5
has not been found so far.
In fact, it is not known if such an axiomatization exists in principle.
However, axiomatizations do exist for a number of fragments of the
language,
obtained by disallowing certain operators, disallowing one or another
sort of
game letters, or imposing some other restrictions on formulas.
In this
section we explore six of such axiomatic
systems: CL7, Int+,
CL15,
CL13, CL4and
CL12. The first four are propositional
systems (only nullary game
letters allowed), while the last two are first-order
systems (no arity restrictions on game letters). CL7,
Int+ and
CL15 are general-base,
meaning that only general game letters are allowed. CL12
is elementary-base, meaning that
only elementary game letters are
allowed. The remaining systems CL13
and CL4 are mixed-base,
allowing both sorts of game letters. The sets ofoperators allowed in formulas are: just{}
for CL7; {, , } for Int+;
{, , , , } for CL15;
{, , , , , , , , } for CL13;
{, , , , , , , , } for CL4;
and { ,,, , , , , , , external } for CL12.
We also divide these systems into the categories Gentzen
style (CL7, Int+),
cirquent calculus (CL15)
and brute force (CL13,CL4,CL12).
Gentzen-style systems are
sequent calculus systems in the traditional sense. It turns out that
only very
limited fragments of CoL can be axiomatized this or any other
traditional (e.g.
Hilbert-style) way, and some novel sorts of proof systems are
necessary.
Cirquent calculus and brute force systems are such novel sorts.
Cirquent
calculus operates with cirquents
rather than
formulas or sequents. Brute force systems operate with formulas or
sequents,
but in an unusual way, with their rules being relatively directly
derived from
the underlined game semantics and hence somewhat resembling games
themselves.
All of
the above systems have been proven to be adequate (sound and complete).
Specifically, we have:
Theorem
6.1.1
Let S
be any one of the systemsCL7, Int+,
CL15,
CL13, CL4or
CL12 defined in the forthcoming
Subsections 6.2-6.7. With “S-formula”
meaning a formula of the language of S
and “S-proof” meaning “proof in S”, we
have:
1. Adequacy:
An S-formula F
is logically valid
iff F is provable in S.
CL7-formulas are formulas
of the language
of CoL that do not contain any function letters, do not
contain any game
letters (including the logical letters and
) other than
nonlogical 0-ary general game letters, and do not contain any operators
other
than .
A CL7-sequent
is a pair Γ⇒F,
where Γ is a
(possibly empty) multiset of CL7-formulas,
and F is a CL7-formula.
As usual,
when Γ and Δ are multisets
of formulas and F is a formula, we
shall write “Γ,Δ” for Γ∪Δ and “Γ,F”
for Γ∪{F}.
The axioms
of CL7 are all CL7-sequents
of the form Γ,F⇒F. And the system
only has the following two rules
of inference:
A CL7-proof
of a sequent S is a sequence X1,…,Xnof
sequents, where S=Xn,
and where each Xi
is
either an axiom or follows from some earlier sequents of the sequenceby one of the rules of
inference. A CL7-proof
of a formula F is a CL7-proof
of the empty-antecedent
sequent ⇒F.
With understood
as linear
implication, CL7 proves nothing
less and nothing
more than the implicative fragment of affine
logic does.
Adding the (left) contraction
rule
to CL7
results in an unsound system. Let us call it CL7+Contraction.
An example of a formula provable in the latter but
not in CL7 is (E(FG))((EF)(EG)). It can be
shown[Jap09b]
however that CL7+Contraction is
sound and complete if we rewrite as
either or
. The logical
behaviors of these two rimplications in isolation are thus
undistinguishable.
This stops being the case when the rimplications are taken in
combination with
other operators. For instance, the intuitionistically provable principle(E⊃G)((F⊃G)⊃(EF⊃G))
is
valid with ⊃read
as but
not as . An example
of a
classical tautology invalid with all three operators ⊃∈{,,} is Peirce’s
Law ((E⊃F)⊃E)⊃E.
Int+-formulas are formulas
of the language
of CoL that do not contain any function letters, do not
contain any game
letters (including the logical letters , ) other than
nonlogical 0-ary general game letters, and do not contain any operators
other
than , , . It turns out
that
logically valid Int+-formulas
are exactly those provable in the positive (negation- and absurd-free)
fragment
of propositional intuitionistic logic Int+.
As a deductive system, Int+
is the result of replacing by
in
the earlier
discussed CL7+Contraction, allowing
and
as
additional operators in
formulas, and
adding the following rules to the system, with i
ranging over {1,2}:
The full
propositional intuitionistic logic Int
is obtained from Int+
by allowing in
the language, and adding
the axiom Γ, ⇒F.
Such a
system is sound but incomplete with respect to our semantics. Below is
an example
of a logically valid yet not Int-provable
principle, with F (the
intuitionistic
negation of F) understood as an
abbreviation
of F:
Does Int+
remain complete with respect to multiform
(rather than uniform) validity?
Add
to the language of Int+,
and adequately axiomatize (if possible) the corresponding
superintuitionistic logic. What kinds of (if any) Kripke models would
such a logic have?
Is the first-order (with
quantifiers ,)positive (negation- and
absurd-free)intuitionistic logic also adequate with respect to
the CoL semantics? If not, could it be axiomatized and how?
Add
to the language of Int+,
but replace the general game letters of the latter with nonlogical
elementary game letters. Adequately axiomatize
(if possible) the corresponding logic.
If the
preceding task is achieved, then try the first-order version of it as
well.
In the
language of Int+, replace with . What logic are we getting? How
about the variations of this logic in the style of the above items 1-5?
CL15-formulas are formulas
of the language
of CoL that do not contain any function letters, do not
contain any game
letters (including the logical letters ,) other than
nonlogical 0-ary general game letters, and do not contain any operators
other
than , , , , . Besides, it
is required
that is
only applied to atoms.
This condition can
be violated if we understand (EF), (EF), E and E as abbreviations of EF,EF, E
and E,
respectively. We may as well write EFor
write EF,understanding these expressions as
abbreviations of EF and EF (i.e. EF),
respectively.
Definition
6.4.1A CL15-cirquent
(hencefore simply
“cirquent”) is a triple C=(F,U,O)
where:
Fis a
nonempty finite sequence ofCL15-formulas,
whose elements are said to be theoformulasofC.Here
the prefix “o” is for “occurrence”, and is used to mean a formula
together with a particular occurrence of it inF.
So, for instance, ifF=〈E,G,E〉, then the
cirquent has three oformulas even ifonly
two formulas.
BothUandOare
nonempty finite sequences of nonempty sets of oformulas ofC.
The elements ofUare
said to be theundergroupsofC,
and the elements ofOare
said to be theovergroupsofC.
As in the case of oformulas, it is possible that two undergroups or two
overgroups are identical as sets (have identicalcontents),
yet they count as different undergroups or overgroups because they
occur at different places in the sequenceUorO.
Simply “group” will be used as a
common name for undergroups and overgroups.
Additionally,
every oformula is required to be in (the content of) at least one
undergroup and at least one overgroup.
While
oformulas are
not the same as formulas, we may often identify an oformula with the
corresponding formula and, for instance, say “the oformula E”
if it is clear from the context which
of the possibly many
occurrences of E is meant.
Similarly,
we may not always be very careful about differentiating between groups
and
their contents.
We represent
cirquents using three-level diagrams such
as the one shown below:
This
diagram
represents the cirquent with four oformulas F1,
F2, F3, F4,
three undergroups {F1},
{F2,F3}, {F3,F4}
and two overgroups {F1,F2,F3},
{F2,F4}. We
typically
do not terminologically differentiate
between cirquents and diagrams: for us, a diagram is
(rather than represents)
a cirquent, and a cirquent is a
diagram.Each (under- or over-) group
isrepresented by a •, where the arcs
(lines connecting the • with
oformulas) are pointing to the oformulas that
the given group contains.
where n is any positive integer, and F1,…,Fn
are any formulas. The diagram of such a cirquent
looks like an array of n
“diamonds”,
as shown below for the case of n=3:
CL15 has nine
rules of
inference. Below we explain them in a relaxed fashion, in terms of
deleting
arcs, swapping oformulas, etc. Such explanations are rather clear, and
translating them into rigorous formulations in the style and terms of Definition 6.4.1, while
possible, is hardly
necessary. All rules take a single premise.
1. Exchange
This
rule
comes in three flavors: Undergroup
Exchange, Oformula
Exchange and Overgroup Exchange.
Each one
allows
us to swap any two adjacent objects (undergroups, oformulas or
overgroups) of a
cirquent, otherwise preserving all oformulas, groups and arcs.
Below
we see
three
examples. In each case, the upper cirquent is the premise and the lower
cirquent is the conclusion of an application of the rule. Between the
two
cirquents --- here and later --- is placed the name of the rule by
which the
conclusion follows from the premise.
The
presence of
Exchange essentially allows us to treat all three components (F,U,O)of a
cirquent as multisets
rather thansequences.
2. Weakening
The
premise of
this rule is obtained from the
conclusion by deleting an arc between some undergroup U
with ≥2 elements and
some
oformula F; if U
was the only undergroup containing F,
then F should also be
deleted (to satisfy Condition 3 of Definition
6.4.1),
together with all arcs between F
and
overgroups; if such a deletion makes some overgroups empty, then they
should
also be deleted (to satisfy Condition 2 of Definition
6.4.1).Below
are three examples:
3.
Contraction The premise
of this rule is obtained from the
conclusion through replacing an oformula F by two
adjacent
oformulas F,F, and
including them
in exactly the same undergroups and overgroups in which the original
oformula
was contained. Example:
4.
Duplication This rule
comes in two versions: Undergroup
Duplication
and Overgroup
Duplication. The conclusion of Undergroup
Duplication is the result of
replacing, in the premise, some undergroup U
with two adjacent undergroups whose contents are identical to that of U. Similarly for Overgroup Duplication.
Examples:
5. Merging In the
top-down view, this rule merges any two
adjacent overgroups, as illustrated below.
6. Disjunction
Introduction The premise
of this
rule is obtained from the conclusion by replacing an oformula FG by two
adjacent
oformulas F,G,
and including both of them in exactly the same undergroups and
overgroups in which the original oformula was contained, as illustrated
below:
7.Conjunction
Introduction The premise of this rule is obtained
from the conclusion
by applying the following two steps:
Replace an
oformula FG by two
adjacent
oformulas F,G,
and include both of them in exactly the same undergroups and
overgroups in which the original oformula was contained.
Replace each
undergroup U originally containing
the oformula FG (and now
containing
F,G
instead) by the two adjacent undergroups U-{G}
and U-{F}.
Below
we see
three
examples.
8.Recurrence
Introduction The premise of this rule is obtained
from the conclusion
through replacing an oformula F by F
(while preserving all arcs), and
inserting, anywhere in the cirquent, a new overgroup that contains F as its only oformula. Examples:
9.
Corecurrence Introduction The premise of
this rule is obtained from the
conclusion through replacing an oformula F by F,
and including F
in any (possibly zero) number of the already existing overgroups
in addition to those in which the original oformula F was already
present. Examples:
A CL15-proof
(or simply a proof in this subsection)of a cirquent C is a
sequence of
cirquents ending in C such that the
first cirquent is an axiom, and every subsequent cirquent follows from
the
immediately preceding cirquent by one of the rules of CL15.
A CL15-proof of
a formula F is understood as a CL15-proof
of the cirquent (〈F〉,〈{F}〉,〈{F}〉), i.e. of the
cirquent
Let us look at
some examples. The following is a proof
of F F, i.e. F F:
The following
example shows a proof of F F F:
At the
same
time,
the converse F F F of the above
formula has no proof. However, the
latter becomes provable after prefixing each occurrence of F
with with . Below is a
proof
ofF F F. The meaningof the principle expressed
by this formula
can be characterized by saying that solving two copies of a problem of
the form
F does not take
any
more resources (is not any harder) than solving just a single copy.
Below
is a proof of F F. Unlike the
previously seen examples, proving this formula requires using
Duplication.
Now we
prove E F (E
F). The
converse (E
F) E F, on the other
hand,
can be shown to be unprovable.
The formulas
proven so far are also provable in affine
logic (with , understood as
multiplicatives, , as
exponentials,
and F as F⊥). In general,
CL15
is a proper
extension of the corresponding (additive-free) fragment of affine
logic. The
following example shows the CL15-provability
of the formula FF,
which is not
provable in affine logic. The converse FF,
on the other hand,
is unprovable in either system.
Another ---
longer but recurrence-free --- example
separating CL15 from affine logic
is
(EF) (GH) (EG) (FH) (the already
mentioned Blass principle),
or even the special
case (EE) (EE) (EE) (EE) of it;
constructing a CL15-proof of this
formula is left as an exercise.
CL15 was
introduced and
proven uniform-constructively adequate
in [Jap13a, Jap13b]. W. Xu and S. Liu
in [Xu13] showed that CL15
remains sound with , instead of,.
Completeness,
however, is lost in this case because, as already
mentioned, the formula F(FFF)F is valid while A(AAA)A is not.
Open
problems 6.4.2
Is CL15 decidable?
Extend the language of CL15 so as to include the
choice connectives and , and axiomatize (if possible) the set
of valid formulas in this extended language.
Replace , with , in the language of CL15. Is the set of valid formulas
in this new language axiomatizable (and how)?
Does CL15 remain complete with respect to
multiform (rather than uniform) validity?
CL13-formulas are formulas
of the language
of CoL that do not contain any function letters, do not
contain any non-nullary game
letters, and
do not contain any operators other than , , , , , , , , . As in the
case of CL15, officially is
only allowed to be
applied to atoms,
otherwise understood as the corresponding DeMorgan abbreviation.EF is also
understood
as an abbreviation of its standard
meaning. To
define the system axiomatically, we need certain terminological
conventions.
As in theprevious
case, we often need to differentiate betweensubformulasas
such, and particularoccurrencesof
subformulas. We will be using the termosubformulato mean
a subformula together with a particular occurrence.The
prefix “o” will be used with a similar meaning in terms such asoatom,oliteral,
etc.
An osubformula
ispositiveiff it
is not in the scopeof. Otherwise it
isnegative.
According to our conventions regarding the usageof, only oatoms
may be negative.
Apoliteralis a
positive oliteral.
A-(sub)formulais a
(sub)formula of the formEF. Similarly
for the other connectives of the language.
Asequential
(sub)formulais one
of the formEForEF. We say thatEis theheadof such
a (sub)formula, andFis itstail.
Similarly, aparallel
(sub)formulais one
of the formEForEF, atoggling
(sub)formulais
one of the formEForEF, and achoice
(sub)formulais
one of the formEForEF.
A formula is
said to bequasielementaryiff it
contains no general atoms and no operators otherthan,,,,.
A formula is
said to beelementaryiff it
is a formula of classical propositional logic, i.e., contains no
general atoms and no operators otherthan,,.
Asemisurface
osubformula(oroccurrence)
is an osubformula (or occurrence) which is not in the scope of a choice
connective.
Asurface
osubformula(oroccurrence)
is an osubformula (or occurrence) which is not in the scope of any
connectives otherthan,,.
Thequasielementarizationof a
formulaF,
denoted by |F|, is the result of replacing inFevery
sequential osubformula by its head, every-osubformulaby, every-osubformula by, and every
general politeral by(the
order of these replacements does not matter). For instance,|((Pq)((pP)(QR))) (q(rs))|=((q)(p)).
Theelementarizationof a
quasielementary formulaF,denotedby ||F||,
is the result of replacing inFevery-osubformulabyand
every-osubformula by(again,
the order of these replacements does not matter). For instance,||(s(p(qr)))(s(pr))||= (s)(s).
A
quasielementary formulaFis said
to bestableiff its
elementarization ||F|| is a tautology of classical
logic. OtherwiseFisunstable.
We now
define CL13 by the following six rules of
inference, where PF means “from
premise(s) Pconclude
F”.
Axioms are not explicitly stated,
but the set of premises of the () rule can be
empty,
in which case (the conclusion of) this rule acts like an axiom.
Rule():H F, where F
is a stable quasielementary formula, and H
is the smallest set of
formulas satisfying the following condition:
WheneverFhas a
surface osubformulaE0E1,
for bothi∈{0,1},Hcontains
the result of replacing inFthat
osubformula byEi.
Rule():HF,
whereFis a
quasielementary formula, andHis the
result of replacing inFa
surface osubformulaEGbyEorG.
Rule():|F|,HF,
whereFis a
non-quasielementary formula (note that otherwiseF=|F|),andHis the
smallest set of formulas satisfying the following two conditions:
WheneverFhas a
semisurface osubformulaG0G1, for bothi∈{0,1},Hcontains
the result of replacing inFthat
osubformula byGi.
WheneverFhas a
semisurface osubformulaEG,Hcontains
the result of replacing inFthat
osubformula byG.
Rule():HF,
where H is the result of replacing inFa
semisurface osubformulaEGbyEorG.
Rule():HF,
whereHis the
result of replacing inFa
semisurface osubformulaEGbyG.
Rule(M):HF,
whereHis the
result of replacing inFtwo ---
one positive and one negative --- semisurface occurrences of some
general atomPby a
nonlogical elementary atompwhich
does not occur inF.
A CL13-proof
of a formula F can be defined as a
sequence of
formulas ending with F such that
every formula follows from some (possibly empty) set of earlier
formulas by one
of the rules of the system.
Example
6.5.1 In
view of
the discussions of Section 3.10,
the formula (pp) (qq) (pq) (pq) expresses
--- or
rather implies --- the known fact that, if two predicates p
and q are
recursively approximable,
then so is their
intersection pq. The
following
sequence is a CL13-proof of this
formula, re-written into its official form ((pp) (qq))
((pq) (pq)):
(pq) (pq)():(no
premises)
(pq) ((pq) (pq))(): 1
(pq) (pq)():(no
premises)
(pq) ((pq) (pq))(): 3
(p (qq)) ((pq) (pq))(): 2,4
(pq) (pq)():(no
premises)
(pq) ((pq) (pq))(): 6
(pq) (pq)():(no
premises)
(pq) ((pq) (pq))(): 8
(p (qq)) ((pq) (pq))(): 7,9
((pp) q) ((pq) (pq))(): 2,7
((pp) q) ((pq) (pq))(): 4,9
((pp) (qq)) ((pq) (pq))(): 5,10,11,12
Example
6.5.2
Pick any two
distinct connectives &1
and &2 from the list,,,. Then CL13
proves the formula P&1Q P&2Q
if and only if &1 is to the left of
&2 in the
list. Similarly for the list ,,,. Below we
verify
this fact only for the case {&1,&2}={,}. The reader
may
want to try some other combinations as exercises.
Here is
a CL13-proof of PQ PQ:
pp():(no
premises)
(p) p(): 1
qq():(no
premises)
(pq)q(): 3
(pQ) Q(M): 4
(pQ) (pQ)(): 2,5
(PQ) (PQ)(M):
6
On the
other
hand,
the formula PQ PQ, i.e. (PQ) (PQ), has no
proof.
This can be shown through attempting and failing to construct,
bottom-up, a
purported CL13-proof of the
formula.
Here we explore one of the branches of a proof-search tree.(PQ) (PQ) is not
quasielementary, so it could not be derived by (be the conclusion of)
the () or () rule.The () rule does
not
apply either, as there is no in
the formula. This leaves
us with one of the
rules (), () and (M). Let
us
see what happens if our target formula is derived by (). In this
case the
premise should beQ (PQ). The latter
can be
derived only by ()or
(M). Again, let us try
(M). The premise in
this subcase should be q (Pq) for some
elementary atom q. But the only way q (Pq)can
be derived is by () from the
premise q (q). This
formula, in
turn, could only be derived by (), in which
case q is one of the
premises. Now we are obviously stuck, as q is not the
conclusion of any of the rules of the system. We thus hit a dead end.All remaining
possibilities can be checked in
a similar routine/analytic way, and the outcome in each case will be a
dead
end.
Exercise
6.5.3
Construct a CL13-proof
of (PP) (PP)(PP).
Exercise
6.5.4
For which of
the four disjunctions ∪∈{,,,} are the
following
formulas CL13-provable and for
which
are not?(1) P∪P;(2) P∪Q Q∪P;(3)
P∪P P;(4)
p∪p p.
Consider the
first-order version of the language of CL13
with choice (to start with) quantifiers. Adequately axiomatize the
corresponding logic.
What is the
computational complexity of (the property of provability in) CL13? (Expectation: PSPACE-complete).
Consider the set of the theorems of CL13 that do not contain nonlogical
elementary letters. Does
this set remain complete
with respect to multiform
(rather than uniform)
validity?
CL4-formulas are formulas
of the language
of CoL that do not contain any operators other than , , , , , , , , .For
simplicity and safety,
we additionally
require that, in any formula, no quantifier binds a variable which also
has a
free occurrence in that formula. As in the previous
cases, negation applied to non-atoms is understood as the
corresponding
DeMorgan abbreviation, and EF is also the
standard abbreviation.An
elementary
CL4-formula is a CL4-formula which
contains no choice
operators and no general game letters. Our axiomatization of CL4 relies on the following terminology
and notation.
AliteralisL(t1,…,tn)
orL(t1,…,tn),
whereL(t1,…,tn)is
an atom. Such a literal is said to beelementaryorgeneraldepending
on whether the letterLis
elementary or general.
Asurface
occurrenceof
a subformula is an occurrence which is not in the scopeof,,, ,and/or.
Theelementarization||F||
of a formulaFis the
result of replacing inFall
surface occurrences of subformulas of the formGH or xGby, all surface
occurrences of subformulas of the formGH orxGby, and all
surface occurrences of general literals by.
A formula is
said to bestableiff its
elementarization is classically valid; otherwise it isunstable.
By “classical validity”, in view of Gödel's completeness theorem, we
mean provability in some fixed standard version of classical
first-order calculus with function letters and =, where = is
the identity predicate (so that, say,x=x,x=y(E(x)↔E(y)), etc. are
provable).
We will be
using the notationF[E1,…,En]
to mean a formulaFtogether
with somenfixedsurface
occurrences of subformulasE1,…,En.
Using this notation sets a context, in whichF[G1,…,Gn]
will mean the result of replacing inF[E1,…,En]
those occurrences ofE1,…,EnbyG1,…,Gn,
respectively. Note that here we are talking about occurrencesofE1,…,En.
Only those occurrences get replaced when moving fromF[E1,…,En]
toF[G1,…,Gn],
even if the formula also had some other occurrences ofE1,…,En.
We now define CL4
by the following four rules
of inference, where PF means “from
premise(s) Pconclude
F”.
Axioms are not explicitly stated,
but the set of premises of the Wait rule can be empty, in which case
(the
conclusion of) this rule acts like an axiom.
-Choose:F[Hi] F[H0H1], where i∈{0,1}.
-Choose:F[H(t)] F[xH(x)],
where t is either a constant or a
variable with no bound occurrences in
the premise.
Wait: E F (n≥0), where F
is stable, and E is a set of formulas
satisfying the following two conditions:
1.
Whenever F has the form F[GH],E contains both F[G] and F[H].
2.
Whenever F has the form F[xG(x)],E
contains F[G(y)] for
some variable y
which does not occur in the conclusion.
Match:F[p(t),p(s)] F[P(t),P(s)], where P
is an n-ary (n³0) general
game
letter, t
and s
are n-tuples of terms, and p
is an n-ary elementary game letter
which does not occur in the conclusion.
The
definitions of
proof and provability in CL4 are
standard. The following is a CL4-proof
ofxy(P(x)
P(y)):
1. p(x)
p(y)Wait: (no premises)
2. P(x)
P(y)Match: 1
3. y(P(z) P(y))-Choose: 2
4. xy(P(x)P(y))Wait: 3
On the
other
hand, CL4 does not proveyx(P(x)
P(y). Indeed, obviously this unstable
formula cannot be the conclusion of any rule but -Choose. If it
is
derived by this rule, the premise should be x(P(x)P(t)) for some
constant
or variable t different from x. x(P(x)P(t)), in turn,
could
only be derived by Wait where, for some variable z
different from t, P(z)P(t)
is a (the) premise. The latter is an
unstable formula and does not contain choice operators, so the only
rule by
which it can be derived is Match, where the premise is p(z)p(t)
for some elementary game letter p.
Now we deal with a classically
non-valid and hence unstable elementary formula, and it cannot be
derived by
any of the four rules of CL4.
Note
that, in
contrast, the “blind version” yx(P(x)
P(y))
of yx(P(x)
P(y))is provable:
1. yx(p(x)
p(y))
Wait: (no premises)
2. yx(P(x)
P(y))Match: 1
‘There
is y such that, for all x,P(x)
P(y)’ is true yet not in a constructive
sense, thus belonging to the kind of principles that have been fueling
controversies between the classically- and constructivistically-minded.As noted earlier, CoL
is offering a peaceful settlement, telling the arguing parties: “There
is no
need to fight at all. It appears that you simply have two different
concepts of
‘thereis’/‘for all’.
So, why
not also use two different names: . / and /. Yes, yx(P(x)
P(y))
is indeed right; and yes, yx(P(x)
P(y)) is indeed
wrong.”Clauses 1
and 2 of Exercise 6.6.1
illustrate a similar solution for the
law of the excluded middle, the most controversial principle of
classical
logic.
The
above-said
remains true with the elementary letter p
instead of the general letter P,
for
what is relevant there is the difference between the constructive and
non-constructive versions of logical operators rather than how atoms
are
understood. Then how about the difference between the elementary and
non-elementary versions of atoms? This distinction allows CoL to again
act in
its noble role of a reconciliator/integrator, but this time between
classical
and linear logics,
telling them: “It appears that
you have two different concepts of the objects that logic is meant to
study.
So, why not also use two different sorts of atoms to represent such
objects:
elementary atoms p,q,…and general atoms P,Q,.... Yes,
ppp is indeed
right;
and yes, PPP (Exercise 6.6.1, clause 4) is
indeed wrong”. However,
the term “linear logic” in this context should be understood in a very
generous
sense, referring not to the particular deductive system proposed by
Girard in [Gir87] but rather to
the general philosophy and intuitions
traditionally associated with it. The formula of clause 3 of the
following
exercise separates CL4 from linear
logic. That formula is provable in affine
logic though.
Switching to affine logic, i.e. restoring the deleted (from classical
logic)
rule of weakening, does not however save the case: the CL4-provable
formulas of clauses 10, 11 and 18 of the following
exercise are provable in neither linear nor affine logics.
Exercise
6.6.1Verify the
following provabilities (Yes:) or
unprovabilities (No:) in CL4.In
clauses 14 and 15
below, provability of E⇔F means
provability ofbothEFandFE.
Taking
into account
that classical validity and hence stability is recursively enumerable,
from the
way CL4 is axiomatized it is
obvious
that the set of theorems of CL4 is
recursively enumerable. Furthermore, it is known from [Jap07a]
that the ,-free fragment
(of
the set of theorems) of CL4 is
decidable in polynomial space. Later M. Bauer [Bau14]
proved
that this fragment is in fact PSPACE-complete. Next, it is a
straightforward
observation that elementary formulas are derivable in CL4
(in particular, from the empty set of premises by Wait) exactly
when they are classically valid. Hence CL4
is a conservative extension of classical predicate logic: the latter is
nothing
but the elementary fragment (i.e. the set of all elementary theorems)
of the
former.
Is the
propositional fragment of CL4
PSPACE-complete?
Consider the set of the theorems of CL4 that do not contain nonlogical
elementary letters. Does
this set remain complete
with respect to multiform
(rather than uniform)
validity?
Try to axiomatize the set of multiformly valid CL4-formulas.
CL12-formulas are formulas
of the language
of CoL that do not contain any general game letters,and do not contain any
operators other than , , , , , , , , . As usual, applied
to non-atoms, as
well as , are
understood as
abbreviations of their official counterparts.
CL12-sequents are
expressions of the form E1,…,EnF
where E1,…,En (n≥0) and F
are CL12-formulas.
Semantically, such a sequent is understood the same
way as the (non-CL12) formula E1…EnF,
so for instance, when we say that the former is logically
valid, we mean
that so is the latter. And a logical
solutionof the former means a logical
solution of the latter.
The language
of CL12
is thus incomparable with that of CL4.
Namely, CL4
allows general game letters while CL12
does not; on the other hand, CL12
allows (uniterated) while
CL4
does not. Due to the presence of ,
CL12 is a very powerful tool for
constructing CoL-based applied theories. It is the logical basis for
all
systems of clarithmetic
(CoL-based arithmetic)
constructed so far. For this reason, CL12
is also the best-studied fragment of CoL, especially from the
complexity-theoretic point of view.[Jap15]Below is some
terminology used in our
axiomatization of CL12. Some terms
have the same meaning as in the case of CL4,
and the meanings of some other terms are “slightly” readjusted.
A surface
occurrence of a subformula is an occurrence that is
not in the scope of
any choice operators.
A formula
not containing choice operators --- i.e., a
formula of the language of classical first order logic --- is said to
be elementary.
A sequent is elementary
iff all of its formulas are so. The elementarization
||F|| of a formula F
is the result of replacing in F all
surface occurrences of - and -subformulas
by , and all - and -subformulas
by . Note that
||F|| is
(indeed) an elementary formula. The elementarization
||G1,…,Gn
F|| of a
sequent G1,…,Gn Fis
the
elementary formula ||G1||…||Gn||
||F||.
A
sequentis said to
be stable
iff its elementarization is classically valid (i.e. provable in some
standard
version of first-order calculus with constants, function letters and
=); otherwise
it is unstable.
We
will be using the notation F[E] to
mean a formula F
together with some (single) fixedsurface occurrence of a subformula E.
Using this notation sets a context,
in which F[H]
will mean the result of replacing in F[E]
that occurrence of E
by H.
Bold-face letters G,K,…
will usually stand for finite sequences of formulas. The standard
meaning of an
expression such as G,F,Kshould
also be clear: this
is the sequence
consisting of the formulas (order respected) of G,
followed by the
formula F, and followed by the
formulas of K.
We now define CL12
by the following six rules
of inference, where PS means “from
premise(s) Pconclude
S”.
Axioms are not explicitly stated,
but the set of premises of the Wait rule can be empty, in which case
(the
conclusion of) this rule acts like an axiom.
3. -Choose:G F[H(t)]G F[xH(x)],
where t is either a constant or a
variable with no bound occurrences in
the premise.
4. -Choose:G, E[H(t)], KFG,
E[xH(x)],
KF,where
t
is either a constant or a variable with no bound occurrences in the
premise.
5.Replicate:G, E,
K,
EFG, E,
K F.
6. Wait:
G1F1, …, GnFnKE(n≥0),where KE is stable and
the
following four conditions are satisfied:
Whenever the
conclusion has the formKE[H0H1], bothKE[H0]
andKE[H1]
are among the premises.
Whenever the
conclusion has the formL,J[H0H1],ME,bothL,J[H0],MEandL,J[H1],MEare
among the premises.
Whenever the
conclusion has the formKE[xH(x)],
for some variableynot
occurring in the conclusion,KE[H(y)]
is among the premises.
Whenever the
conclusion has the formL,J[xH(x)],ME,for
some variableynot
occurring in the conclusion,L,J[H(y)],MEis
among the premises.
Each
rule ---
seen
bottom-up --- encodes an action that a winning strategy should take in
a
corresponding situation, and the name of each rule is suggestive of
that action.
For instance, Wait (indeed) prescribes the strategy to wait till the
adversary
moves. This explains why we have called“Replicate” the rule which otherwise is nothing but what
is commonly
known as Contraction.
A CL12-proof
of a sequent S is a sequence S1,…,Sn
of sequents, with Sn
=S, such that each Si
followsby one of
the rules of CL12 from some
(possibly empty in the case of Wait, and certainly
empty in the case of i=1) set P of premises
such that P⊆ {S1,…,Si-1}.
A CL12-proof of a
formula F is understood as a CL12-proof
of the empty-antecedent
sequentF. Whether it
be a
sequent or a formula, “provable
in CL12”, of course, means “has a CL12-proof”.
The uniform-constructive adequacy theorem
stated earlier for
all systems of this section extends without changes from CL12-formulas
to CL12-sequents,
understanding each such sequent E1,…,EnF
as
the (non-CL12) formula E1…EnF.
CL12 is a
conservative extension of classical logic. That is, an elementary
sequent E1,…,EnF
is
provable in CL12 iff the formula E1…EnFis valid in the classical
sense. This is an
immediate corollary of the adequacy
theorem for CL12. But
this fact can also be easily
verified directly. Indeed, assume E1,…,En,F are
elementary
formulas. Note that then the elementarization
of E1,…,EnF is
E1…EnF.
If the latter is classically valid, then E1,…,EnF
follows from the empty set of premises by Wait. And if E1…EnF
is
not classically valid, then E1,…,EnFcannot be the conclusion
of any of the rules
of CL12 except Replicate. However,
applying (bottom-up) Replicate does not take us any closer to finding a
proof
of the sequent, as the premise still remains an unstable elementary
sequent.
Example
6.7.1 In this
example,✕ is a binary
function letter and 3 is a
unary function letter. We write x✕y and x3
instead of ✕(x,y)
and 3(x),
respectively.
The following sequence of sequents is a CL12-proof of its last sequent.
1.x(x3= (x✕x)✕x),t=s✕s, r=t✕sr=s3Wait: (no premises)
Exercise
6.7.2To see the
resource-consciousness of CL12,
show
that it does not prove pq (pq)(pq), even though
this
formula has the form FFF of a
classical
tautology. Then show that, in contrast, CL12
proves the sequentpq (pq)(pq) because,
unlike
the antecedent of a -combination,
the
antecedent of a -combination
is reusable
(trough Replicate).
Exercise
6.7.3
Show that CL12
proves xyp(x,y)x(yp(x,y) y p(x,y)). Then observe
that,
on the other hand, CL12 does not
prove any of the formulas
xyp(x,y) x(yp(x,y) y p(x,y));
xyp(x,y) xyp(x,y)x(yp(x,y) y p(x,y));
xyp(x,y)xyp(x,y) xyp(x,y)x(yp(x,y) y p(x,y));
…
Intuitively,
this contrast is due to the fact that,
even thoughboth A and A = AAA… are resources
allowing to reuse A any number of
times, the “branching” form of reusage offered by A is
substantially
stronger than the “parallel” form of reusage offered by A.xyp(x,y)x(yp(x,y) yp(x,y)) is a valid
principle of CoL while xyp(x,y)x(yp(x,y) yp(x,y))is
not.
1. A CL12-sequent is
provable in CL12 iff it is logically
valid.
2. There
is an effective procedure which takes an arbitrary CL12-proof
of an arbitrary CL12-sequent
GF and
constructs a
linear amplitude, constant space and linear time logical
solution of GF.
Thus, every
cirquent either has a very efficient
logical solution (as efficient as it gets), or no logical solution
solution at
all.
We say
that a CL12-formula F
is a logical
consequence of CL12-formulasE1,…,En (n≥0) iff CL12
proves the sequent E1,…,En
F.
The
following
rule,
which we (also) call Logical
Consequence (LC),
will be the only logical rule of inference in CL12-based
applied systems:
E1,…,EnF,where
F is a logical consequence ofE1,…,En.
Remember
that, philosophically speaking, computational resources
are symmetric to computational problems: what is a
problem for one player to solve is a resource that the other player can
use.
Namely, having a problem A as a
computational resource intuitively means having the (perhaps externally
provided) ability to successfully solve/win A.
For instance, as a resource, xy(y=x2)
means the ability to tell the square of any number.According to the following thesis, logical
consequence lives up to its name:
Thesis
6.7.5Assume E1,…,Enand F
are CL12-formulas
such thatthere is a *-independent (whatever interpretation *)
intuitive
description and justification of a winning strategy for F*,
which relies on the availability and “recyclability” --- in the
strongest sense possible --- of E1*,…,En*as
computational
resources.Then
F is a logical consequence of E1,…,En.
Example
6.7.6
Imagine a CL12-based
applied formal theory, in which we have already proven x(x3=(x✕x)✕x) (the meaning
of“cube” in terms of multiplication) and xyz(z=x✕y) (the
computability of multiplication), and now we
want to derive xy(y=x3)
(the computability of “cube”). This is how we can reason to justify xy(y=x3):
Consider any s
(selected by Environment for x in xy(y=x3)).
We need to find s3.
Using the resource xyz(z=x✕y),we first find the value t of s✕s, and
thenthe value r of t✕s.
According
to x(x3=(x✕x)✕x), such an
r is
the
sought s3.
Thesis 6.7.5 promises that the
above intuitive argument
will be translatable into a CL12-proof
of
x(x3=(x✕x)✕x), xyz(z=x✕y) xy(y=x3)
(and
hence the
succedent xy(y=x3)
will be derivable in thetheory
by LC as
the formulas of the antecedent are already proven). Such a proof indeed
exists
--- see Example 6.7.1.
While Thesis 6.7.5 is about
the completeness of LC,
the following Theorems 6.7.7
and 6.7.8 are about soundness,
establishing that LC preserves computability, and does so in a certain
very
strong sense. It is these two theorems to which CL12
(LC, that is) owes its appeal as a logical basis for
complexity-oriented applied theories. Theorem
6.7.7
carries good news for the cases where time efficiency is of main
concern, and
otherwise we are willing to settle for at least linear space.Theorem
6.7.8
does the same but for the cases where the primary concern is space
efficiency
--- namely, when we want to keep the latter sublinear. These theorems
use the
term “native magnitude”,
by which, for a sequent S, we mean
the greatest of all constants (here seen as the
corresponding natural numbers) that appear in S,
or 0 is there are no constants in S.
Theorem
6.7.7 There is aneffective procedure which
takes an arbitrary CL12-proofP of an
arbitrary CL12-sequent E1,…,En
F,
arbitrary HPMsN1,…,Nn
and constructs anHPMM
such that the following holds:
Assume
* is an interpretation and a,s,t
are unary arithmetical functions such that:
For each i∈{1,…,n},
Niis
an a
amplitude, s space and t time
solution of Ei*.
For any x,a(x)≥max(x,c),
wherec
is the native magnitude of E1,…,En
F.
For any x,s(x)≥x.
For any x,t(x)≥x.
Then
thre is
a
number b which only depends on P such that,
with R
abbreviating ab(y),M is a solution of F* which
runs in amplitude R,
space O(s(R)) and time O(t(R)).
Theorem
6.7.8There is aneffective procedure which takes an arbitrary CL12-proofP of an
arbitrary CL12-sequent
E1,…,En F,
arbitrary HPMsN1,…,Nn
and constructs anHPMM
such that the following holds:
Assume
* is an interpretation and a,s,t
are unary arithmetical functions such that:
For each i∈{1,…,n},
Niis
an a
amplitude, s space and t time
solution of Ei*.
For any x,a(x)≥max(x,c),
wherec
is the native magnitude of E1,…,EnF.
For any x, s(x)≥log(x).
For any x,t(x)≥x and t(x)≥s(x).
Then there is
are
numbers b,d
which only depend on P such that,
with R abbreviating ab(y),M
is a solution of F* which runs in
amplitude R, space O(s(R)) and time O((t(R))d).
Add the
sequential connectives , to the language of CL12 and adequately axiomatize the
corresponding logic.
Try to axiomatize the set of multiformly
valid CL12-sequents.
Along with elementary game letters, allow
also general game letters in the language of CL12, and try to axiomatize the set
of valid sequents of this extended language.
}
for CL7; {
, 
, 
} for Int+;
{
, 
, 
, 
, 
} for CL15;
{
, 
, 
, 
} for CL13;
{
, 
, 
, 
} for CL4;
and {
F