| |
 |
|
|
Science Forum Index » Logic Forum » Predicate logic axioms...
Page 1 of 1
|
| Author |
Message |
| Scott H... |
 Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
Wikipedia's list of rules of inference give the following rules of predicate
logic:
P
-------
Aa P
Aa P
-------
P(b/a)
P(b/a)
-------
Ea P
Ea P
P |- Q
-------
Q
However, I thought of something simpler:
Aa P(a)
-------
P(a)
P(a)
-------
Ea P(a)
Aa P(a)
P(a) -> Q(a)
-------
Aa Q(a)
Ea P(a)
P(a) -> Q
-------
Q
I do not even invoke the idea of a free term. Are the latter four axioms
standard? |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 7:42 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:
Quote: Review the definitions of 'satisfaction' and of the 'soundness
theorem' and you will see that my demonstration is correct.
P.S. A rule that IS sound is:
AxPx
Ax(Px -> Qx)
______
AxQx
MoeBlee |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 7:18 pm, "Scott H" <nospam> wrote:
Quote: MoeBlee wrote:
On Jun 17, 6:10 pm, "Scott H" <nospam> wrote:
But 'x' denotes a free variable. How is Qx ("x is even") derived
from Px ("x is a number") for arbitrary x?
What I did is an assignment for the free variables. A sound inference
rule must preserve truth not just for closed formulas but also
preserve satisfaction of open formulas too. My example shows a model
and an assignment for the free variables such that the premises are
satisfied but the conclusion is not. A sound inference rule does not
allow such a situation.
With my axioms and under my rules, Px -> Qx is only derivable using an
actual free variable 'x'. No assignment may be made.
No, the assignment is in the SEMANTICS, in a model and assignment of
values to the variables.
A sound rule preserves SATISFACTION. That is, a sound rule is such
that every model and assignment for the variables that satisifes the
premises also satisfies the conclusion. I showed a model and
assignment in which the premises are satisfied but the conclusion is
not satisfied. That demonstrates that the rule is not sound (in the
sense that the soundness theorem does not hold for a system with your
rule).
Quote: The universalizability
of Qx, as a consequence of that of Px, is thereby preserved, as the free
variable 'x' is syntactically treated as arbitrary in the derivation.
Whatever you say about that doesn't vitiate the correct SEMANTICAL
refutation I gave.
Quote: I do not yet see a flaw in this system.
Review the definitions of 'satisfaction' and of the 'soundness
theorem' and you will see that my demonstration is correct.
MoeBlee |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 6:33 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:
Quote: 1 AxPx ... supposition {1}
2 Px -> Qx ... supposition {2}
3 ~Qx ... supposition {3}
4 ~Px ... 2, 3
5 Px ... 1 {1}
6 Qx ... 3, 4, 5 by contradiction {1, 2}
7 AxQx ... 6 by universal generalization {1 2} WRONG
Line 7 is WRONG, because x is free in line 2.
I didn't need contradiction. Even simpler:
1 AxPx ... supposition {1}
2 Px -> Qx ... supposition {2}
3 Px ... 1 {1}
4 Qx ... 2, 3 {1 2}
5 AxQx ... 4 {1 2} WRONG (x is free in line 2)
MoeBlee |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 6:33 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:
Quote: the antecedent (Qx) is satisfied.
I meant
the consequent (Qx) is satisfied.
MoeBlee |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 6:10 pm, "Scott H" <nospam> wrote:
Quote: MoeBlee wrote:
Rule 3 is refuted:
Let the universe U = the set of natural numbers.
Map P to U.
Map Q to the set of even numbers.
Map x to 2.
Then
AxPx is true
Px -> Qx is true
but
AxQx is false.
But 'x' denotes a free variable. How is Qx ("x is even") derived from Px ("x
is a number") for arbitrary x?
What I did is an assignment for the free variables. A sound inference
rule must preserve truth not just for closed formulas but also
preserve satisfaction of open formulas too. My example shows a model
and an assignment for the free variables such that the premises are
satisfied but the conclusion is not. A sound inference rule does not
allow such a situation.
Once I've made an assignment for the free variables, x has a
"temporary" denotation. In this case,
Px -> Qx
is satisfied in the model per the assignment to the variables since
the antecedent (Qx) is satisfied.
And you can see where the argument breaks down in an ordinary
calculus:
1 AxPx ... supposition {1}
2 Px -> Qx ... supposition {2}
3 ~Qx ... supposition {3}
4 ~Px ... 2, 3
5 Px ... 1 {1}
6 Qx ... 3, 4, 5 by contradiction {1, 2}
7 AxQx ... 6 by universal generalization {1 2} WRONG
Line 7 is WRONG, because x is free in line 2.
Quote: I thought "free term" and "free variable" meant different things. If they
don't, I apologize for the confusion.
I don't know about all usages, but I go with pretty ordinary usage:
free variable
bound variable
open term
closed term
open formua
closed formula (sentence)
term free for variable in formula
formula free for sentence letter in formula
MoeBlee |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 5:44 pm, MoeBlee <jazzm... at (no spam) hotmail.com> wrote:
Quote: I do not even invoke the idea of a free term.
If at least part of your interest is to have rules without
restrictions on variables, then you might find something to help you
at the metamath web site. He uses workarounds to not have to mention
variable restrictions in some of his formulations. However, I don't
know whether his particular techniques would work in the context of
the rest of your system.
MoeBlee |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 4:55 pm, "Scott H" <nospam> wrote:
Quote: MoeBlee wrote:
On Jun 17, 4:42 pm, "Scott H" <nospam> wrote:
However, I thought of something simpler:
Aa P(a)
-------
P(a)
P(a)
-------
Ea P(a)
Aa P(a)
P(a) -> Q(a)
-------
Aa Q(a)
Ea P(a)
P(a) -> Q
-------
Q
I do not even invoke the idea of a free term. Are the latter four
axioms standard?
No, because it's not sound. It's a trivial exercise for you to prove
that.
Help me out a little here. How are my axioms unsound?
Your last rule (call it 'rule 4') permits, for example, inferring Px
from ExPx, as follows:
1 ExPx ... supposition {1}
2 Px -> Px ... tautology
3 Px ... 1, 2 rule 4 {1}
Rule 3 is refuted:
Let the universe U = the set of natural numbers.
Map P to U.
Map Q to the set of even numbers.
Map x to 2.
Then
AxPx is true
Px -> Qx is true
but
AxQx is false.
Rules 1 and 2 are both sound, but if you corrected rules 3 and 4,
then rules 1 and 2 would be too weak (e.g., how would you ever derive
alphabetic variance, or that matter how would you derive Fx from
AyFy?).
MoeBlee |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Tue Jun 17, 2008 6:42 pm |
|
|
|
Guest
|
On Jun 17, 4:42 pm, "Scott H" <nospam> wrote:
Quote: However, I thought of something simpler:
Aa P(a)
-------
P(a)
P(a)
-------
Ea P(a)
Aa P(a)
P(a) -> Q(a)
-------
Aa Q(a)
Ea P(a)
P(a) -> Q
-------
Q
I do not even invoke the idea of a free term. Are the latter four axioms
standard?
No, because it's not sound. It's a trivial exercise for you to prove
that.
MoeBlee |
|
|
| Back to top |
|
| Scott H... |
| Posted: Tue Jun 17, 2008 6:55 pm |
|
|
|
Guest
|
MoeBlee wrote:
Quote: On Jun 17, 4:42 pm, "Scott H" <nospam> wrote:
However, I thought of something simpler:
Aa P(a)
-------
P(a)
P(a)
-------
Ea P(a)
Aa P(a)
P(a) -> Q(a)
-------
Aa Q(a)
Ea P(a)
P(a) -> Q
-------
Q
I do not even invoke the idea of a free term. Are the latter four
axioms standard?
No, because it's not sound. It's a trivial exercise for you to prove
that.
Help me out a little here. How are my axioms unsound? |
|
|
| Back to top |
|
| Scott H... |
| Posted: Tue Jun 17, 2008 8:10 pm |
|
|
|
Guest
|
MoeBlee wrote:
Quote: On Jun 17, 4:42 pm, "Scott H" <nospam> wrote:
Aa P(a)
P(a) -> Q(a)
-------
Aa Q(a)
[snip]
Quote: Rule 3 is refuted:
Let the universe U = the set of natural numbers.
Map P to U.
Map Q to the set of even numbers.
Map x to 2.
Then
AxPx is true
Px -> Qx is true
but
AxQx is false.
But 'x' denotes a free variable. How is Qx ("x is even") derived from Px ("x
is a number") for arbitrary x?
I thought "free term" and "free variable" meant different things. If they
don't, I apologize for the confusion. |
|
|
| Back to top |
|
| Scott H... |
| Posted: Tue Jun 17, 2008 9:18 pm |
|
|
|
Guest
|
MoeBlee wrote:
Quote: On Jun 17, 6:10 pm, "Scott H" <nospam> wrote:
But 'x' denotes a free variable. How is Qx ("x is even") derived
from Px ("x is a number") for arbitrary x?
What I did is an assignment for the free variables. A sound inference
rule must preserve truth not just for closed formulas but also
preserve satisfaction of open formulas too. My example shows a model
and an assignment for the free variables such that the premises are
satisfied but the conclusion is not. A sound inference rule does not
allow such a situation.
With my axioms and under my rules, Px -> Qx is only derivable using an
actual free variable 'x'. No assignment may be made. The universalizability
of Qx, as a consequence of that of Px, is thereby preserved, as the free
variable 'x' is syntactically treated as arbitrary in the derivation.
I do not yet see a flaw in this system. |
|
|
| Back to top |
|
| MoeBlee... |
| Posted: Thu Jun 19, 2008 3:21 pm |
|
|
|
Guest
|
On Jun 19, 5:21 pm, "Scott H" <nospam> wrote:
Quote: The three axioms for quantifiers given in Angelo Margaris' _First Order
Mathematical Logic_ on p. 49 are:
Av(P -> Q) -> (AvP -> AvQ)
AvP -> P(t/v)
P -> AvP, when v is not free in P
Nice axioms. Very trad. Except, doesn't the author say about the
second one that it requires that t is free for v in P? (Also, be
careful whether open formulas are allowed as axioms or not. This is a
nit, but just to be precise it comes in when we consider that a theory
is a set of SENTENCES closed under entailment).
Quote: I'm guessing that P(t/v) is a shorthand for
Et(Q(t) & Ar(Q(r) -> r = t))
-> Et(Q(t) & Ar(Q(r) -> r = t) & P(t))
where Q defines the term.
I don't see how that could be correct. First of all, unless Margaris
has something else in mind, 't' is a term, which is not necessarily a
variable, so you can't write "Et".
Later tonight I can look up to see whether Margaris is indeed using
the usual definitions, but in the meantime, here's the usual rundown
(as you will find in Enderton and other books):
First we have an inductive definition of
s[t|v] where s and t are terms and v is a variable (this is an
inductive way of saying that s[t|v] is the result of replacing all
free occurrences of v by t):
If s is a constant symbol, then s[t|v] is s.
If s is a variable and s is not v, then s[t|v] is s.
If s is v, then s[t|v] is v is t.
If s is ft_1...t_n where t_1, ..., t_n are terms and f is an n-place
function symbol, then
s[t|v] is ft_1[t|v]...t_n[t|v].
Next, we have an inductive definition of P[t|v] where P is a formula
(this is an inductive way of saying P[t|v] is the result of replacing
all free occurrences of v by t):
If P is a sentence letter, then P[t|v] is P.
If P is Ft_1...t_n where t_1, ..., t_n are terms and F is an n-place
predicate symbol,
then P[t|v] is Ft_1[t|v]...t_n[t|v].
If P is ~Q, then P[t|v] is ~(Q[t|v]).
If P is Q -> R, then P[t|v] is Q[t|v] -> R[t|v].
If P is AxQ, and x is a variable, and x is not v, then P[t|v] is
Ax(Q[t|v]).
If P is AxQ, and x is v, then P[t|v] is AxQ is P.
Then you also need the definition of "t is free for v in P" which is
given inductively (as a way of saying that substituting t for v
doesn't cause any new occurrences of bound variables):
If P is atomic, then t is free for v in P.
If P is ~Q, then t is free for v in P iff t is free for v in Q.
If P is Q -> R, then t is free for v in P iff both t is free for v in
Q and t is free for v in R.
If P is AxQ, then t is free for v in P iff either v does not occur in
P or both x does not occur (free) in t and t is free for v in Q.
(Officially, I don't need the parenthesized '(free)', but I include it
just for informal ease where t is a "term" made with a variable
binding operator.)
And all of those inductive definitions are strictly formalized by
functions proven to exist by definition by recursion theorems.
Quote: For completeness, the other axioms are:
P -> (Q -> P)
(S -> (P -> Q)) -> ((S -> P) -> (S -> Q))
(~Q -> ~P) -> (P -> Q)
AvP, when P is an axiom and v is free in P
Okay, but I like better the way Enderton formulates virtually this
same axiomatization but such that only sentences are axioms, so that
last clasue about AvP is not needed (as well as v doesn't have to be
free in P since there is no harm in vacuous quantification)..
Quote: and the rule of inference is Modus Ponens.
Yep.
What's next?
MoeBlee |
|
|
| Back to top |
|
| Scott H... |
| Posted: Thu Jun 19, 2008 7:21 pm |
|
|
|
Guest
|
MoeBlee wrote:
Quote: On Jun 17, 7:18 pm, "Scott H" <nospam> wrote:
With my axioms and under my rules, Px -> Qx is only derivable using
an actual free variable 'x'. No assignment may be made.
No, the assignment is in the SEMANTICS, in a model and assignment of
values to the variables.
I see. Maybe I was being a bit careless in replacing |- with ->.
The three axioms for quantifiers given in Angelo Margaris' _First Order
Mathematical Logic_ on p. 49 are:
Av(P -> Q) -> (AvP -> AvQ)
AvP -> P(t/v)
P -> AvP, when v is not free in P
I'm guessing that P(t/v) is a shorthand for
Et(Q(t) & Ar(Q(r) -> r = t))
-> Et(Q(t) & Ar(Q(r) -> r = t) & P(t))
where Q defines the term.
For completeness, the other axioms are:
P -> (Q -> P)
(S -> (P -> Q)) -> ((S -> P) -> (S -> Q))
(~Q -> ~P) -> (P -> Q)
AvP, when P is an axiom and v is free in P
and the rule of inference is Modus Ponens. |
|
|
| Back to top |
|
| |
|
Page 1 of 1
All times are GMT - 5 Hours
The time now is Sat Sep 06, 2008 2:26 pm
|
|