Transcript Infinite Models for Propositional Calculi

Infinite Models for
Propositional Calculi
Zachary Ernst
University of Missouri-Columbia
[email protected]
The Gist
Finite matrix models are equivalent to
finite state bottom-up tree automata.
 So perhaps, more powerful automata can
play the role of infinite matrix models.

The Problem
Finite matrix models are good for showing
that formulae are not theorems of
propositional logics.
 But many systems require infinite models.
 These are hard to enumerate, and there
is no good, flexible framework for
describing them.

Another Example

System due to J. Anderson:
Cxx
 CCIxxy (where Ix=Cxx)
 CCIxyxCCIIxyz
 Modus Ponens and Universal Substitution


Theorems are all of the form:

CCIII…Ixxy, for any number of I’s.
A “Hyperfinite” System

Anderson’s system is “hyperfinite”:


Any finite model that respects modus ponens
and uniform substitution validates every
formula.
This is easy to show, and the proof is
informative about the limits of finite
models.
The Proof
Consider the following infinite sequence of theorems:
Ix
IIx
IIIx
…
IIIIIIx
III…Ix
…
The Proof
If M is some arbitrary finite matrix model…
Ix
IIx
IIIx
…
IIIIIIx
III…Ix
…
…then there must be
some pair of formulae in
the sequence that M
“identifies”.
The Proof
Ix
IIx
IIIx
…
IIIIIIx
III…Ix
…
Suppose M “thinks” that
IIx = IIIIIIx.
The Proof
Ix
IIx
IIIx
…
Suppose M “thinks” that
IIx = IIIIIIx.
IIIIIIx
III…Ix
Then according to M:
…
CIIIIIIxIIx = Cxx, which is a theorem.
The Proof
According to M:
CIIIIIIxIIx = Cxx, which is a theorem.
Now consider:
CCIIIIIIxIIxy=CCIIII(IIx)(IIx)y, which is of the form:
CCIII…IXXY, which is a theorem (where X=IIx).
The Proof
According to M:
CIIIIIIxIIx = Cxx, which is a theorem.
Now consider:
CCIIIIIIxIIxy=CCIIII(IIx)(IIx)y, which is of the form:
CCIII…IXXY, which is a theorem (where X=IIx).
So one application of modus ponens yields y.
Therefore, the model must validate everything.
What Happened?




Finite matrix models must “identify” two
elements of any sufficiently long list of formulae.
So it will incorrectly think that when those
formulae are combined, the resulting formula
will be equivalent to Cxx.
No finite matrix model validates exactly the
instances of Cxx (Gödel).
If Cxx is a theorem, then the model will validate
the formula.
How to Use a Matrix Model
1
2
1
1
2
2
1
1
CpCqq
p
q
q
How to Use a Matrix Model
CpCqq
1
1
p
1
q
q
2
2
1
2
1
1
2
2
1
1
Finite Matrices as Finite
Automata


Using a finite matrix
model is like letting
an automaton run
over a tree.
“Designated Values”
are like “Accept
States”.
CpCqq
1
1
p
1
q
q
2
2
The Disanalogy -- Vocabulary
Finite tree automata have a finite input
language.
 Logics have an infinite language with
countably many variables.


This matters for models, but not for
countermodels.
Restricting the Input Vocabulary


Suppose {Cpq, r}s, by condensed
detachment, and suppose s has fewer distinct
variables than one of the premises.
Then there is a substitution  such that:



p= r; q=s, and
Cpq and r have no variables not appearing in s.
Therefore, if P is a set of premises, and there is
a proof of C from P, then there is a proof of C
from P containing only variables occurring in C.
Restricting the Input Vocabulary



So we know in advance how many variables
are necessary for a proof of C from P, if such a
proof exists.
Thus, we do not need a countermodel
containing infinitely many variables; if C has a
single variable, then the countermodel is only
required have an interpretation for only one
variable.
So it does not matter that tree automata have a
finite input language; they still might serve as
countermodels.
A Stronger Automaton

Weighted Tree Automata use weights from a
semiring:
 Suppose semiring is   R,,,0,1
 Every transition has a transition cost from R



The costs for each successful run are multiplied
using the semiring multiplication.
The total costs
 for all runs are added using the

semiring addition.
The automaton accepts a tree if the cost associated
with the tree is in some subset J  R
Are Weighted Automata Strong
Enough for Infinite Models?
For some infinite sequence of formulae, a
weighted automaton must be able to
assign a different weight to each member
of the sequence.
 It is easy to construct an automaton that
calculates the binary value of a tree. In
other words, there is an automaton such
that A( p)  0, A(Cpp)  4, A(CpCpp)  20

Weighted Automata and
Reflexivity
Recall that Gödel showed that no finite
model accepts exactly the instances of
Cxx.
 But if the binary value of   BIN ( ) then
there is an automaton such that:

A(C)  BIN()  BIN()  0 iff   .


Terminology: We say that A “0-accepts” only the
instances of Cxx.
Weighted Automata and
Anderson’s Hyperfinite System
Recall that the theorems of Anderson’s
k

T

{CCI
xxy
|
k

N
}
system are
 We can construct an automaton such
that: if   CCC, and the length of x  x , then




So let
A( )  2  3  5 
J  {n  N |n  2 k 3k5 l ,l  k}
YQE
Show that CCxyCCxzCyz does not imply
CxCyCxy, with the rule modus ponens
and uniform substitution.
 Ted Ulrich has shown that if YQE does
not imply CxCyCxy, then it will take an
infinite model to show this.
