[FOM] Re: Combining classical and intuitionistic features in one logic

[Matthew Frank]

I originally sent this message to Alex Sakharov privately; since he said
that it does answer his question, I am now forwarding it to the whole
list.  --Matt

---------- Forwarded message ----------
Date: Sun, 15 Feb 2004 18:42:16 -0600 (CST)
From: Matthew Frank <mfrank at tachyon.uchicago.edu>
To: "mail at sakharov.net" <sakharov at earthlink.net>

Dear Alex,

I read with interest your recent fom post about combining classical and
intuitionistic logics, particularly combining models based on truth tables
with the disjunction and existence properties.

I have an argument that you're not going to find any logic with both of
these properties, as follows:

First, I restrict to the propositional case.  In the light of Harvey
Friedman's result that the disjunction property and numerical existence
property are equivalent for most reasonable arithmetic theories, I don't
think this is such a big restriction.  (See ``On the derivability of
instantiation properties", JSL 42 (1977), 506-514.)

Second, I reformulate the disjunction property.  The main trick is to
formulate the disjunction property without referring to disjunction!
After all, any candidate intermediate logic is likely to have unfamiliar
connectives, with unfamiliar properties from the odd set of truth
values--so it might happen that no connective is well described as
"disjunction", or it might happen that multiple connectives are well
described as "disjunction".  The secondary trick is to use a semantic
version of the disjunction property (corresponding to "P or Q" is valid
iff P is valid or Q is valid), since the truth-table set up is already
semantic.


Now for the technicalities:

A truth-table logic is given by a truth-table T and a set of propositional
connectives, where each n-ary connective corresponds to a map from T^n to
T.  We assume that one truth-value is denoted "true".  If phi is a
proposition using the propositional variables P_1, ... P_n, let true(phi)
be the set of ordered n-tuples of truth values which make phi true.  So
phi is valid if true(phi) contains all n-tuples of truth values.
Likewise phi entails theta iff true(phi) is contained in true(theta).

Def.:  The pair of propositions {phi,psi} is *disjunctively valid* iff
whenever phi entails theta, and psi entails theta, then theta is valid.

Def.:  A truth-table logic *satisfies the semantic disjunction property*
iff whenever {P,Q} is disjunctively valid, either P is valid or Q is
valid.

I claim that the correspondingly defined syntactic disjunction property
(i.e. with entailment and validity defined syntactically) holds for all
for formal systems ordinarily proved to satisfy the ordinary disjunction
property, and fails for all ordinary classical formal systems.  Therefore
I think this is a reasonable definition.


With these preliminaries we get a trivial but possibly enlightening

Theorem:  Suppose that a truth-table logic contains propositions phi and
psi such that phi is not valid, and psi is not valid, but for any
particular combination of truth-values either phi or psi is true at that
combination of truth-values.  Then the logic does not satisfy the semantic
disjunction property.

Proof:  The only propositions entailed by both phi and psi are the valid
propositions; therefore {phi, psi} is disjunctively valid.  However
neither phi nor psi is valid.

The hypothesis is weak:  it simply asserts that (for some n) T^n is
expressible as a non-trivial union of two propostions.  It is hard to
imagine any truth-table logic with reasonable expressive power that
violates this condition.


I think these ideas are simple and answer your question in a strong way.
I hope they haven't been confused by technicalities.

--Matt