Robert Wasierski wrote:
>I guess this kinda stuff confuses me because of the
>assumptions.
>
>
>
>> Now let us consider whether her father is telling
>> the truth. Suppose
>> Sally is good and he does take her. In this case
>> his statement is true.
>
>Are we using symbology to analyze someone's statement?
>
>In boolean algebra, we don't care what the values are.
>We use symbology to define the behavior of a system
>described with a boolean algebra statement.
>
>Here it appears we are implying:
>
> 1. That there is a statement.
>
>
> 2. That there is an expression.
>
> 3. That the <IF> statement attempts to formalize
> the relationship between a statement and an
> expression and express them with a second
> statement.
>
>This is much different from the use of logic to define
>a logic circuit. The final expression is the result of
>an input expression and a statement (algebraic
>formula), resulting in an output statement.
>
>My biggest problem in understanding this kind of
>language or dialog is the difference I just described.
>
>Robert Wasierski
For the sake of future convenience I will be a little more
precise. I sum up also.
Here is a set {p, q, r, ...} which element are called
propositional variables.
It will be useful to take also a constant FALSE.
They represent, or are intended for, atomic propositions, but
this does not concern the left brain.
You can define well formed formula (wff) recursively, and
I propose this:
0) FALSE is a well formed formula,
1) p, q , r ... are well formed formula,
1) if A and B are wff then A -> B
And nothing else.
I propose you take
-A as an abbreviation of A -> FALSE
(The right brain can provide a motivation: FALSE
is intended for representing the proposition which is always
false, and then, note that the truth value of "A -> FALSE" are
always opposite to the truth value of A. Like -A.
A & B is an abbreviation of -(A -> -B)
which, BTW, abbreviates ((A -> (B -> FALSE)) -> FALSE)
A v B is an abbreviation of (-A) -> B
A <-> B is an abbreviation of (A -> B) & (B -> A)
TRUE is an abbreviation of -FALSE.
Now what is sometime called the proof theory, or the syntactical
approach, or more simply the left brain view is that
You have a theory.
By definition, a theory is a set of well formed formula called
axioms, in company of a set of inference rules or simply rules.
See the preceding post for the Hilbert Ackerman theory. It has
three axioms and the rules: modus ponens.
A theorem is a wff you can proof (or a machine can proof, at least
here it is provably equivalent) with those axioms and those rules.
And this without any reference to any meaning or truth value
of the formula.
It happens that Classical logic has the "truth table semantics"
(see preceding post). A tautology or valid wwf is a wwf true for
all valuation of its atomic constituant.
What is worth to remember is that
the set of theorems (Th) in the Hilbert Ackerman (HA)
theory is equal to the to the set of tautologies (Ta).
soundness of HA: Th included in Ta
completeness of HA: Ta is included in Th.
OK ?
Don't be too nervous on formal details, we will meet
more and more theories and semantics, so a lot of
things will became more familiar with time.
Now for S5 (just add [] and <> in the set of connectives,
so we have as connectives {->, [], <>}
we can take the following system (to avoid
messy substitution rule in the logic, I present the
system directly with axioms schema. That is
A -> (B -> A) represent all the well formed formula
p -> (q -> p), ((p -> p) -> (q -> (p -> p)) etc.
Propositional Axioms
A->(B->A)
(A->B)->(-A->-B) where -A is really A->FALSE
(A->(B->C))->((A->B)->(A->C))
Modal Axioms
[](A->B) -> ([]A -> []B)
[]A->A
<>A -> []<>A
Rules: A A->B (Modus Ponens)
----------
B
and A (necessitation rule).
---
[]A
Let us call again Th the set of theorems in S5 (left brain)
and Ta the set of all valid formulas (true in all Leibniz model
(= right brain) see one of the preceding posts)
Then we have (we will prove or see hints toward proof later):
soundness of S5: Th included in Ta
completeness of S5: Ta is included in Th.
OK?
Bruno
Received on Fri Mar 30 2001 - 09:06:20 PST
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:07 PST