Thanks Hal,
For a while I thought that Bruno and I inhabited portions of the Plenitude
with different logics (modal logic).
hal.domain.name.hidden wrote:
> > >> A v B A -> B
> > >> 1 1 1 1 1 1
> > >> 1 1 0 1 0 0
> > >> 0 1 1 0 1 1
> > >> 0 0 0 0 1 0
>
> Just to help you guys out, the notation used here puts the 'result'
> operation in the middle column. The first column is A, the last column
> is B, and the middle column holds "A or B" in the first table and "if A
> then B" in the second table. This is different than how I have usually
> seen it displayed, where the result operation is in the rightmost column.
> That accounts for part of the confusion.
>
> Hal
Thanks Bruno for the course in logic.
Every thing so far, is understandable (possibly knowable :-) ), but I will
have to read and reread that stuff several times. To make this job easier, I
started a binder just for Bruno's posts. It will make it easier for me to go
back and forth. And forgive me for not being too prompt with my replies....
Let's just make sure we agree upon our objectives. Did we agree then that, the
proof we are striving for is the derivation of Planck's constant for purely
philosophical arguments? Or is it the full Schroedinger equation in all its
details? I still maintain that whoever derives the actual digits of that
constant (in MKS units for example) will *at least* deserve a Nobel or
better.. *At present,* it seems so impossible to me, that, I believe the
prize should be given by a prestidigitation organization. :-). It will
certainly be instructive to go through that process.
George
Marchal wrote:
> George Levy wrote:
>
> >With my background in electronic engineering, I am moderately versed in
> >logic, in particular Boolean logic. I am sorry for my long hmmmm. The
> >going got rough when you started talking about knowability and
> >believability. But I realize that if we are to investigate consciousness
> >these are ideas that have to be talked about.
>
> Yes.
>
> >So let's go with it.. I promise I'll give it a shot.
>
> Take your time for ruminating this.
>
> >It will be very
> >instructive.... However it would help if together with the string of
> >symbols there was an English translation.
>
> OK. Just tell me when you don't understand.
>
> >> The semantics of well formed formula like p & (q v r)
> >> will follow by the usual use of truth table. For exemple:
> >>
> >> A v B A -> B
> >> 1 1 1 1 1 1
> >> 1 1 0 1 0 0
> >> 0 1 1 0 1 1
> >> 0 0 0 0 1 0
> >
> >hmmm.... do you mean?
> >
> > A v B A -> B
> > 1 1 1 1 1 1
> > 1 0 1 1 0 0
> > 0 1 1 0 1 x
> > 0 0 0 0 1 x
>
> In classical propositional logic the "or" is inclusive. That is
> A v B is true by definition in case A is true or B is true or if both
> A and B are true. The latin has a word for both "or": *vel* (inclusive
> logical or, and *aut* exclusive logical or).
>
> By definition A -> B is false only when it is falsifiable, that is when
> A is true and B false. In fact A -> B can be considered as an
> abreviation of -(A & -B). It is called *material implication* and is
> a priori special. C.L. Lewis (re)invented Logic last century (20) in part
> for capturing more reasonable "implication" (by [](p -> q)).
>
> Note that it made p->(q->p) a tautology. A formula true for any
> valuations. Some philosophical logician consider that as a "paradox":
> we have indeed: "the fact that I am a flying pig *materially implies*
> the truth of Fermat last theorem", and also "the fact that I am a flying
> pig materially implies the fact that Moscow is the capital of USA".
> Of course it is not a contradiction (with what we know!) unless you find
> a proof (or any real evidence) that *I am a flying pig*.
> Just interpret the intended meaning of "p->q" as a shortand
> of -(p & -q).
>
> I guess you know "de Morgan laws": -(A & B) <-> -A v -B
> -(A v B) <-> -A & -B
>
> We have also A -> B is equivalent with -B -> -A
>
> "Equivalent" is taken here either in the intuitive meaning, or
> in the sense that the formula ((A -> B) <-> (-B -> -A)) is a
> tautology (true for all valuations) as we can verify exhaustively:
>
> ((A -> B) <-> (-B -> -A))
> 1 1 1 1 01 1 01
> 1 0 0 1 10 0 01
> 0 1 1 1 01 1 10
> 0 1 0 1 10 1 10
>
> using the table for p <-> q
>
> A <-> B or if you prefer <->1 0 (like a multiplication table)
> 1 1 1 1 1 0
> 1 0 0 0 0 1
> 0 0 1
> 0 1 0
>
> or by saying that (A <-> B) is an abbreviation of (A->B) & (B->A).
>
> >> Exercices. Show that the following sentences are valid:
> >>
> >> p -> <>p
> >> []p -> [][]p
> >> p -> []<>p
> >> <>p -> []<>p
> >> [](p->q) -> ([]p -> []q)
> >>
> >> Of course if <>p -> []<>p is valid, <>TRUE -> []<>TRUE is
> >> certainly valid to, and so our "godel second theorem"
> >> <>TRUE -> -[]<>TRUE is certainly NOT valid with Leibniz
> >> semantics. This just means that formal provability cannot
> >> play the role of the leibnizian "necessity".
> >> Kripke generalisation of Leibniz semantics will provide
> >> the necessary tools.
> >>
> >
> >OK
>
> Nice. If someone has not see that <>p -> []<>p is valid
> in Leibnizian semantics, please insist for explanation. But we
> will explain it again with the Kripkian semantics, actually.
>
> >> The non logician should note that with a semantics we can
> >> reason on the validity of sentences without having a formal
> >> system in which we could *prove* those formula.
> >> A "difficult" exercice would consist in finding a formal
> >> system which would axiomatize the Leibnizian formula.
> >>
> >> (In fact it is axiomatized by the system known as S5 which
> >> has the axioms:
> >>
> >> [](p->q) -> ([]p -> []q)
> >> []p->p
> >> <>p -> []<>p
> >>
> >> + the classical tautologies.
> >>
> >> with the inferences rules:
> >>
> >> p p->q p
> >> ------- --- + a substitution rule
> >> q []p
> >>
> >
> >This string of symbols does not mean anything to me... Is there a real
> >life model to which it applies, a story, a game, anything to give it
> >meaning?
>
> There is a lot of (boring) games, for sure!
>
> I explain it firstly for classical propositional logic itself.
>
> You know, for a logician, a theory is just a set of formulas, called
> axioms,
> and a set of rules of inference, from which new formulas (called theorems)
> can be derived.
>
> For exemple, here is the Hilbert Ackerman axiomatisation (theory) of
> Classical Propositionnal Logic.
>
> It is a theory with the following 3 axioms:
>
> Axiome a p -> (q -> p)
> Axiome b (p -> q) -> (-q -> -p)
> Axiome c (p -> (q -> r)) -> ((p -> q) -> (p -> r))
>
> Now, if there is no inference rules, you cannot prove any theorems,
> except the three axioms themselves.
>
> An inference rule is a recipe which make possible to derive new
> formula (called theorems) from the axioms.
>
> The two rules of Hilbert Ackerman are 1) the substitution rule
> and 2) the modus ponens rule.
>
> The substitution rule is awkward to describe precisely, but it just
> says that you can make careful substitution. So you can derive
> from the first axiom q -> (p -> q) or ((p -> r) -> (q -> (p -> r)), etc.
>
> The very fundamental rule we will have in all logics is the modus
> ponens: it is written (and I explain what that means after!):
>
> A A -> B
> ------------ Modus Ponens
> B
>
> It means that if you have found a proof of A and if you have found a
> proof of A -> B, then you can deduce B (and now you have a proof of B).
>
> What is a (formal) proof ? It is just a sequence of formula which are
> either
> axioms or which are deduced from the axioms or from theorems (which has
> been obtained until now) by a finite number of application of the rule
> of inference. A formal proof is just a syntactical derivation which should
> be "mechanicaly" verifiable.
>
> Exemple or game!
> Find a proof of the formula p -> p in the Hilbert Ackerman system.
>
> (It is a little tricky, and nobody should waste his/her time
> on such boring exercice). But it is nice for illustrating what is an
> axiomatic system and what are proofs in that system).
> But it is worth to verify that the following solution is indeed
> a proof.
>
> The solution:
>
> 1) (p -> ((p -> p) -> p)) -> ((p -> (p -> p)) -> (p -> p))
> This is an instance of axiome c with the substitution
> q/(p -> p) r/p
>
> 2) (p -> ((p -> p) -> p))
> This is an instance of axiome a with the subst. q/(p -> p)
>
> 3) (p -> (p -> p)) -> (p -> p)
> This follows from 1 and 2 by the Modus Ponens rule
>
> 4) (p -> (p -> p))
> This follow from axiome a with the subst. q/p
>
> 5) p -> p
> This follows from 3) and 4) by Modus Ponens again.
>
> Now you will tell me: why ? It is much more easy to look at
> the truth table, isn't it.
> The answer is multiple. 1) The difficulty comes here from the fact
> that the Hilbert Ackermann axiomatic theory is very concise. 2) Most
> logical system have no truth table. 3) (And this is the main point)
> the interesting thing are the relation between the syntactical
> and combinatorial world of the proofs and the semantical world of
> the worlds in which these truth applies.
>
> You should convince yourself that
>
> 1) All formulas provable in the Hilbert Ackerman system are tautologies.
> This is not difficult. Just verify that the axioms are tautologies
> and that tautologicalness is preserved by the application of the
> rules of inference. We say that the Hilbert Ackerman axiomatic is
> SOUND with respect to classical (truth table) semantics.
>
> 2) All tautologies are provable in the Hilbert Ackerman axiomatic.
> Actually this is not easy. I will explain later how to prove similar
> result. We say that the Hilbert Ackerman axiomatic is
> COMPLETE with respect to classical (truth table) semantics.
>
> Remember that a logician has two brains (like everyone), a left
> brain and a right brain. The left brain understand only formal
> mechanical but "easily" communicable (verifiable) proofs, the right
> brain understands only semantics, meaning, attribution of truth values
> to proposition in worlds.
> A logician is happy when he has a formal system with both
> a theory (axioms and rules)
> a semantics (a mathematical structure ...., we will see)
> accompagnied by a soundness result (the theory proofs correct theorems
> with respect to the semantics), and a completeness result (the theory
> proofs all formulas which are true with respect to the semantics).
>
> "Modern logic" can be said to be the science of the communication
> between the left and the right brain, if you accept the image.
>
> Let us go back to S5:
>
> >> [](p->q) -> ([]p -> []q)
> >> []p->p
> >> <>p -> []<>p
> >>
> >> + the classical tautologies.
> >>
> >> with the inferences rules:
> >>
> >> p p->q p
> >> ------- --- + a substitution rule
> >> q []p
>
> Of course the necessitation rule (p/[]p) just say that if you
> have find a proof of A, then you can deduce []A. In particular
> <>p -> []<>p being a theorem (it is an axiom, so it is trivialy
> a theorem!), [](<>p -> []<>p), [][](<>p -> []<>p),
> [][][](<>p -> []<>p), are also
> theorems by simple application of the necessitation rule.
>
> We have completeness and soundness of S5 with respect to
> Leibniz semantics: S5 proves A if and only if A is valid
> in all the (Leibnizian) worlds.
> As always, soundness is more easy to prove that completeness.
> I will give later hint to prove completeness for the
> modal logics.
>
> Could you prove in S5 that p -> []<>p ? With the completeness
> result, we know there is a proof! (because p -> []<>p is
> Leibnizian valid as we have suggest as an exercice
> in the preceding post).
>
> Semantics are also useful to prove decidability and other
> nice (meta)logical properties of theories.
>
> >Thanks for making this effort.
>
> Thanks for your effort and your patience.
>
> Bruno
Received on Wed Mar 28 2001 - 14:22:02 PST
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:07 PST