| |
 |
|
|
Science Forum Index » Logic Forum » Cont.: How does metamath deal with PA's axiom 15?...
Page 1 of 1
|
| Author |
Message |
| Jan Burse... |
 Posted: Tue Jun 03, 2008 2:44 pm |
|
|
|
Guest
|
Dear All
In sept 2007 there was a post:
Quote: I'm at page 66 of Hirst's paper, the axioms for PA.
I noticed that axiom 15 is "an infinite axiom schema."
How does metamath deal with this kind of axiom?
Answer was:
Quote: In Metamath's case, one can use a "wff variable" that ranges
over all possible formulas.
...
Yes, the resolution algorithm does not work with schemes but
only with specific instances of them.
Ok, thus non-scheme variables x will have the
following rule:
x [x/t] = t
y [x/t] = y, for x<>y
But a scheme variable A will not have any rule,
we simply need to put a substitution on hold,
until the variable A is further instantiated:
A [x/y] put on hold
My question is. Is it possible to give to these
scheme variables a model theoretic semantic?
For non-scheme variables we can do the following:
Define an environment s as a mapping from variables
to elements of the universe of domain.
s : V -> U
When there is also an interpretation for function
symbols, we can extend it to terms:
s f(x1,..,xn) := f(s x1,..,s xn)
Clearly we have the following identity:
s p[x/q] = s' p
where
s'(y) := if x=y then s(q) else s(y)
Is there a similar syntactic semantic link(*) for
non scheme variables? How can such a link work when
have things "on hold"?
Best Regards
(*) I have some ideas, but lets first see whether there
are already some canonical solutions. |
|
|
| Back to top |
|
| Jan Burse... |
| Posted: Tue Jun 03, 2008 2:46 pm |
|
|
|
Guest
|
Jan Burse schrieb:
Quote: Is there a similar syntactic semantic link(*) for
non scheme variables?
Oops, question should read:
Is there a similar syntactic semantic link(*) for
*scheme* variables? |
|
|
| Back to top |
|
| |
|
Page 1 of 1
All times are GMT - 5 Hours
The time now is Mon Oct 06, 2008 12:52 pm
|
|