| View previous topic :: View next topic |
| Author |
Message |
Chris Menzel Guest
|
Posted: Wed Jul 16, 2008 8:49 pm Post subject: Re: completeness what is it exactly |
|
|
On Wed, 16 Jul 2008 13:25:27 -0700 (PDT), translogi
<wilemien@googlemail.com> said:
[quote]On Jul 16, 8:13 pm, Jan Burse <janbu...@fastmail.fm> wrote:
herbzet schrieb:
Would someone please explain to me why propositional logic
does not have variables? Or does not have free variables?
Or whatever? I must have missed the memo.
Your propositional formulae at the bottom of this post sure look to
me like they contain free variables.
No, they are zero arity predicate constants.
Bye
Do I now still understand it
(Or am i just getting totally confused)
p-> p
p is a sentence letter
(or equivalent an 0 -place predicate symbol)
(or a zero arity predicate constants
(or a propositional variable)
[ any other name for this concept ;-) ]
Is therefore p->p a sentence?
But if p->p is a sentence then also (p->p)->p is a sentence.
[/quote]
p->p is not a sentence in standard grammars for propositional logic. If
it were, so would p->p->p. But this "sentence" is ambiguous depending
on whether we group to the right or left. Parentheses are therefore
essential for avoiding ambiguity in languages that use so-called "infix"
operators (instead of "prefix" operators as in languages that use Polish
notation). A typical grammar for a propositional language containing
only the logical operators ~ and -> would be:
1. Every sentence letter is a sentence.
2. If A is a sentence, so is ~A.
3. If A and B are sentences, so is (A->B).
4. Nothing else is a sentence.
Given this grammar, we can then, as a *convention*, drop the outer
parentheses when writing sentences of the form (A->B), as doing so does
not lead to any ambiguity in the assignment of truth values.
[quote]Back to Completeness.
negation completeness says
for every sentence A
|- A or |- ~A
[/quote]
Well, not in general. Negation completeness is a property of
*theories*, i.e., deductively closed sets of sentences. So the proper
definition is: A theory T is negation complete if, for any sentence A of
the language of T, either T |- A or T |- ~A.
[quote]But still neither |- (p->p)->p nor |- ~((p->p)->p)
[/quote]
Or more simply, we have neither |-p nor |-~p, for sentence letters p.
So the theory consisting solely of the theorems of propositional logic
is not negation complete.
[quote]therefore:
- (p->p) ->p is not a sentence
[/quote]
Whether a string is a sentence is solely a matter of the grammar of the
language. It has absolutely nothing to do with its provability.
[quote]- propositional logic is not negation complete
[/quote]
Correct. Propositional logic is *semantically* complete, that is, every
tautology of the semantics is a theorem of the proof theory, i.e., as it
is usually expressed in the metatheory for propositional logic:
If |=A, then |-A. |
|
| |
|
Back to top |
MoeBlee Guest
|
Posted: Wed Jul 16, 2008 9:35 pm Post subject: Re: completeness what is it exactly |
|
|
On Jul 16, 1:25 pm, translogi <wilem...@googlemail.com> wrote:
[quote]p is a sentence letter
(or equivalent an 0 -place predicate symbol)
(or a zero arity predicate constants
(or a propositional variable)
[ any other name for this concept ;-) ]
Is therefore p->p a sentence?
[/quote]
Yes. For the sixth time, yes. It is a sentence because there are no
free variables in it (where 'variables' is in the sense of those
things you can put after a quantifier or have occurrences in the scope
of a quantifier so as to be bound by that quantifier or not in the
scope of a quantifier so as to be free, where 'quantifier' is in the
sense of a quantifier in the same language as the language of the
variable).
[quote]But if p->p is a sentence then also (p->p)->p is a sentence.
[/quote]
Yes, so?
[quote](if what a sentence is is only defined by syntax)
[/quote]
'sentence' is a syntactical term. A sentence is a well formed formula
that has no occurrences of free variables.
[quote]Back to Completeness.
negation completeness says
for every sentence A
|- A or |- ~A
But still neither |- (p->p)->p nor |- ~((p->p)->p)
[/quote]
No. If 'p' is a sentential letter (a 0-place predicate symbol), and a
set G of formulas is negation complete, then either G proves (p->p)->p
or G proves ~((p->p)->p).
[quote]therefore:
- (p->p) ->p is not a sentence
- propositional logic is not negation complete
or
something else all together????
[/quote]
No, why are you having trouble here?
If p is a sentence letter (in either propositional logic or predicate
logic), then
(p->p) ->p
is a sentence.
[quote]replacing sentence letter p with Q
where Q stands for any propositional
formula, (then this is a schema, and not
a formula.)
Q -> Q
and
(Q->Q) ->Q
[/quote]
Correct. 'Q' is an individual variable in the META-language now. And
we could say, "For all Q, if Q is a formula [...]", or "For all Q, if
Q is a sentence [...]", depending on which we mean, or we just make an
informal convention that Q ranges over sentences or over formulas, or
over whatever, as the case may be.
[quote]are they both sentences?
only the first one?
neither of them?
(that only the second is a sentence nobody will have that opinion)
[/quote]
No, if 'Q' is a variable in the meta-language, then 'Q -> Q' and '(Q -
[quote](Q -> Q)' are open TERMS in the metalanguage. They are terms in the
meta-language with the free-variable 'Q'. If we were to fully[/quote]
formalize,
for Q->Q
we would actually have
the concatenation of Q with '->' with Q,
which is a TERM. The expression "the concatenation of Q with '->' with
Q" is a term, a definite description. But it>s an open term since 'Q'
is a variable. It>s a variable and not a sentence because it is NOT a
sentence letter in the meta-lanaguage in which it is being used, but
rather a variable RANGING OVER formulas (or sentences, whatever we
stipulate) of the OBJECT language.
[quote]If
Axiom A has sentence letters,
and
Sentences are formula>s without sentence letters (Or propositional
variables)
[/quote]
No, sentences are formulas without free variables. Sentences can have
occurrences of sentence letters.
[quote]Sentences are formula>s without sentence letters cut any wood.
(Still think it doesn>t)
[/quote]
You>re right, it doesn>t. Because it>s not the definition.
[quote]Defining axioms as sentences feels a bit the wrong way round.
[/quote]
No, it makes perfect sense. We want a theory to be a set of sentences
not just a set of formulas; and we want the axioms themselves to be
members of the theory, so we stipulate that an axiom must be a
sentence.
[quote](Completeness means that if formula A is true then formula A is
provable)
[/quote]
That is a DIFFERENT sense of completeness. We>re not talking about
that sense of completeness. Also, it does not make sense to talk about
a formula being true if it is not known that the formula is a
sentence. Open formulas are not true or false in a model; rather open
formulas are satifisfied or not satisified in a model with an
assignment to the variables.
[quote]so starting with defining axioms as sentences looks at least weird.
[/quote]
We DON>T define axioms as sentences. We REQUIRE that axioms be
sentences but that is not ALL that we require in the definition of
'axiom'. And the "weirdness" you imagine goes away when you realize
you>ve conflated two different senses of 'complete'.
[quote]So it all goes back to the question
What is a Sentence?
(Other than what is a well formed formula)
[/quote]
If it goes back, then it goes back for the tenth time now. We told you
what a sentence is:
Something is a sentence iff it is a formula with no occurrences of
free variables.
[quote]still confused
[/quote]
Really, there shouldn>t be confusion. It couldn>t be more clear:
Something is a sentence iff it is a formula with no occurrences of
free variables.
More formally,
S is a sentence of L iff (L is a language and S is a formula of L and
S has no occurrences of free variables per L)
MoeBlee |
|
| |
|
Back to top |
MoeBlee Guest
|
Posted: Wed Jul 16, 2008 9:44 pm Post subject: Re: completeness what is it exactly |
|
|
On Jul 16, 2:35 pm, MoeBlee <jazzm...@hotmail.com> wrote:
[quote]On Jul 16, 1:25 pm, translogi <wilem...@googlemail.com> wrote:
Is therefore p->p a sentence?
Yes. For the sixth time, yes.
[/quote]
P.S. I just noticed that Chris Menzel gave a different answer, based
on the consideration that parentheses are needed so that the sentence
is actually
(p -> p).
So, please take my remarks to have the tacit stipulation that I>m
considering your formulas as if they are making use of such informal
conventions as dropped outer parentheses and things like that. And
that goes right along with the rest of Chris>s remarks in that regard.
MoeBlee |
|
| |
|
Back to top |
Jan Burse Guest
|
Posted: Thu Jul 17, 2008 12:13 am Post subject: Re: completeness what is it exactly |
|
|
herbzet schrieb:
[quote]Would someone please explain to me why propositional logic
does not have variables? Or does not have free variables?
Or whatever? I must have missed the memo.
Your propositional formulae at the bottom of this post
sure look to me like they contain free variables.
[/quote]
No, they are zero arity predicate constants.
Bye |
|
| |
|
Back to top |
Jan Burse Guest
|
Posted: Thu Jul 17, 2008 2:20 am Post subject: Re: completeness what is it exactly |
|
|
translogi schrieb:
[quote]But still neither |- (p->p)->p nor |- ~((p->p)->p)
therefore:
- (p->p) ->p is not a sentence
- propositional logic is not negation complete
or
something else all together????
[/quote]
The empty theory is not complete.
Recall the definition:
complete(T) :<=> forall A in L (T |- A v T |- ~A)
Now you showed:
{} |/- (p->p)->p
{} |/- ~((p->p)->p)
(Lets assume this is correct)
Conclusion:
~complete({})
And this is indeed the case, the empty theory is
not complete.
(Of course the empty theory is not complete,
as it does not have any domain axioms in it,
so its totally defensive, only logical)
(~complete(_), or incomplete means there is
a sentence A and a model M1 of T, and a model
M2 of T, with M1[A]=0 and M2[A]=1. Of course we
can have models of {} with M1[p]=0 and M2[p]=1.
Thus also M1[(p->p)->p]=0 and M2[(p->p)->p]=1)
Bye |
|
| |
|
Back to top |
MoeBlee Guest
|
Posted: Thu Jul 17, 2008 3:57 am Post subject: Re: completeness what is it exactly |
|
|
On Jul 16, 7:33 pm, herbzet <herb...@gmail.com> wrote:
[quote]MoeBlee wrote:
and we may regard 't' and 'f' (for 'truth' and 'falsehood') as 0-ary
connectives.
That>s new (to me) and amusing. We get the slightly odd-sounding
situation of wffs consisting of only connectives (e.g. 't v f')!
[/quote]
True, it is odd, even oxymoronic sounding terminology, and interesting
observation you discovered about a formula made of only connectives
(that hadn>t occurred to me before). On the other hand, for certain
treatments, the terminology does make for a nice, tidy way of
organizing the symbols.
Sometimes our definitions do lead to odd situations. For example {1}
is a function. Yes, just the singleton of the natural number 1 is a
function:
{1} = {{0}} = {{0} {0 0}} = {<0 0>} is a function.
[quote]I guess this preference comes from the fact that axiom systems
for '|' or 'dagger' are not well known and pretty unintuitive.
[/quote]
Actually, it came from that problem you helped me out with several
months ago. I had wanted a single primitive, but then you proved that
I was on the wrong track thinking I couldn>t get the system on the
cheap by just taking the Lesniewski axioms (or is it Lukaciewz [sp]? I
forgot, so I>ll call it 'L') "as if" they were for the Sheffer stroke.
So I decided it was better anyway just to use an ordinary ~ -> system,
for sake of not getting bogged down with axioms harder to intuit and
read. Also, using ~ -> makes my system more familiar to most readers
[quote]If you want to make '|' or 'dagger' your sole primitive connective
you could take as propositional axioms the set of "all tautologies",
since this is a decidable set (just make a truth table for a given
formula). Some authors, e.g. Quine, take this approach. Also
Enderton, I think.
[/quote]
Yes, Enderton for sure. But I chose not to do that since, for my own
self-pedagogy (and for anyone who might read my notes) I want to
include all the steps that go into proving that all the tautologies
are provable from the L axioms (which are axioms probably as common as
any other set). Then, also, I define a natural deduction system (and
without trees, but rather with sequences of ordered pairs with the
first coordinate of each ordered pair being a formula and the second
coordinate being the set of formulas upon which the deduction of said
formula depends upon at that point in the proof, i.e., pretty much a
pedantically strict formulation of a system such as found in Mates and
other books); then I prove that the L system is equivalent with my
natural deduction system.
[quote]For set theory:
Extension of identity theory.
Add the 2-place predicate symbol 'e'.
Since '=' is so easily defined with 'e'
x = y =def Az [z e x <-> z e y] (iirc)
why not just have one primitive predicate? Does this wreak
havoc with the axiom of extension?
[/quote]
No, it only requires an easy-to-formulate alternative version of
extensionality with the definition of '='. And that>s fine. But for my
own purposes, for the way I have the chapters in my notebook laid out,
I find it just as well to take set theory as an extension of identity
theory, which is also a common approach.
[quote]Or is it perhaps that you like the convenience of having a
background logic that contains '=' as primitive but is not
wedded to set theory?
[/quote]
Yes, that>s very much part of it. With identity theory, we can do all
the needed theorems in one separate chapter, as a kind of "portable
module" that we can then hook up to the rest of our mathematical
theories such as set theory, PA, etc. That is, once we do all the
identity theory stuff, we don>t have to redo it each time we go for a
mathematical theory that turns out to be the same set of theorems as
an extension of identity theory anyway.
MoeBlee |
|
| |
|
Back to top |
herbzet Guest
|
Posted: Thu Jul 17, 2008 7:32 am Post subject: Re: completeness what is it exactly |
|
|
MoeBlee wrote:
[quote]herbzet wrote:
MoeBlee wrote:
And in pure propositional
logic, there are no open formulas, since there are no free variables
anywhere, since there are no variables at all.
What??? What do you call p, q, r, etc.?
I call them 'sentence letters'.
In this context, by 'variable' we (I) mean 'individual
variable' (i.e., the ones used in predicate logic that are, e.g., free
or bound).
[/quote]
[etc.]
Thanks, MoeBlee, for a nice post.
--
hz |
|
| |
|
Back to top |
herbzet Guest
|
Posted: Thu Jul 17, 2008 7:33 am Post subject: Re: completeness what is it exactly |
|
|
MoeBlee wrote:
[quote]herbzet wrote:
MoeBlee wrote:
[/quote]
Just a few comments:
[...]
[quote]and we may regard 't' and 'f' (for 'truth' and 'falsehood') as 0-ary
connectives.
[/quote]
That>s new (to me) and amusing. We get the slightly odd-sounding
situation of wffs consisting of only connectives (e.g. 't v f')!
[...]
[quote]My own preference for first order language is:
n-place predicate symbols
n-place function symbols
connectives - ~ -> (with & v <-> | 'dagger' t f defined)
[/quote]
I guess this preference comes from the fact that axiom systems
for '|' or 'dagger' are not well known and pretty unintuitive.
If you want to make '|' or 'dagger' your sole primitive connective
you could take as propositional axioms the set of "all tautologies",
since this is a decidable set (just make a truth table for a given
formula). Some authors, e.g. Quine, take this approach. Also
Enderton, I think.
[...]
[quote]For set theory:
Extension of identity theory.
Add the 2-place predicate symbol 'e'.
[/quote]
Since '=' is so easily defined with 'e'
x = y =def Az [z e x <-> z e y] (iirc)
why not just have one primitive predicate? Does this wreak
havoc with the axiom of extension?
Or is it perhaps that you like the convenience of having a
background logic that contains '=' as primitive but is not
wedded to set theory?
[quote]Define set abstraction notation from the iota operator.
[/quote]
--
hz |
|
| |
|
Back to top |
herbzet Guest
|
Posted: Thu Jul 17, 2008 7:33 am Post subject: Re: completeness what is it exactly |
|
|
Jan Burse wrote:
[quote]herbzet schrieb:
Would someone please explain to me why propositional logic
does not have variables? Or does not have free variables?
Or whatever? I must have missed the memo.
Your propositional formulae at the bottom of this post
sure look to me like they contain free variables.
No, they are zero arity predicate constants.
[/quote]
Hokay! (An elegant dodge!)
--
hz |
|
| |
|
Back to top |
Jan Burse Guest
|
Posted: Thu Jul 17, 2008 12:01 pm Post subject: Re: completeness what is it exactly |
|
|
MoeBlee schrieb:
[quote]On Jul 16, 7:33 pm, herbzet <herb...@gmail.com> wrote:
MoeBlee wrote:
and we may regard 't' and 'f' (for 'truth' and 'falsehood') as 0-ary
connectives.
That>s new (to me) and amusing. We get the slightly odd-sounding
situation of wffs consisting of only connectives (e.g. 't v f')!
True, it is odd, even oxymoronic sounding terminology, and interesting
observation you discovered about a formula made of only connectives
(that hadn>t occurred to me before). On the other hand, for certain
treatments, the terminology does make for a nice, tidy way of
organizing the symbols.
[/quote]
Connectives and quantifiers can also be viewed as constants. Namely:
v : prop -> (prop -> prop)
& : prop -> (prop -> prop)
~ : prop -> prop
-> : prop -> (prop -> prop)
<-> : prop -> (prop -> prop)
f : prop
t : prop
forall : (domain -> prop) -> prop
exists : (domain -> prop) -> prop
Some of the constants can be considered defined by other ones.
1-ary predicates have the following signature:
pred : domain -> prop
And variables have the following signature:
var : domain
An easy meta logic can use lambda expressions to express formulas.
So a formula:
forall x (p(x) -> q(x))
Is in fact a lambda expression:
(forall lambda x.(-> (p x) (q x)))
We can check whether the above is a term or a formula, by checking
whether it has type domain or type prop. The only typing rules we
need to apply are:
A : T1 -> T2 B : T1
------------------------
(A B) : T2
x : T1 A : T2
-------------------------
lambda x.A : T1 -> T2
By this rule our formula has the following type:
p : domain -> prop x : domain q : domain -> prop x : domain
-------------------------------- ------------------------------
(p x) : prop (q x) : prop
-> : prop -> (prop -> prop) (p x) : prop
----------------------------------------------
(-> (p x)) : prop -> prop
(-> (p x)) : prop -> prop (q x) : prop
------------------------------------------------
(-> (p x) (q x)) : prop
x : domain (-> (p x) (q x)) : prop
--------------------------------------
lambda x.(-> (p x) (q x)) : domain -> prop
forall:(domain->prop)->prop lambda x.(->(p x)(q x)):domain->prop
-----------------------------------------------------------------
(forall lambda x.(->(p x)(q x))) : prop
Bye |
|
| |
|
Back to top |
MoeBlee Guest
|
Posted: Thu Jul 17, 2008 5:24 pm Post subject: Re: completeness what is it exactly |
|
|
On Jul 16, 8:57 pm, MoeBlee <jazzm...@hotmail.com> wrote:
[quote]For example {1}
is a function. Yes, just the singleton of the natural number 1 is a
function:
{1} = {{0}} = {{0} {0 0}} = {<0 0>} is a function.
[/quote]
Darn, I meant this:
{1} is an ordered pair, and {{1}} is a function.
{1} = {{0}} = {{0} {0 0}} = <0 0> is an ordered pair.
{{1}} = {<0 0>} is a bijection from {0} onto {0}
It would be interesting to put the question on a set theory exam:
True or false (and explain your answer): {1} is an ordered pair.
Another trivial case: 1 is a topology on 0, so <0 1> is a topological
space. (Here /\0 = 0, using the Fregean method for improperly
referring descriptions.)
MoeBlee |
|
| |
|
Back to top |
MoeBlee Guest
|
Posted: Thu Jul 17, 2008 5:34 pm Post subject: Re: completeness what is it exactly |
|
|
On Jul 16, 8:57 pm, MoeBlee <jazzm...@hotmail.com> wrote:
[quote]On Jul 16, 7:33 pm, herbzet <herb...@gmail.com> wrote:
MoeBlee wrote:
and we may regard 't' and 'f' (for 'truth' and 'falsehood') as 0-ary
connectives.
That>s new (to me) and amusing. We get the slightly odd-sounding
situation of wffs consisting of only connectives (e.g. 't v f')!
[/quote]
Ah, now that I think about it, what you just said jogged my memory: I
misspoke. Yes, one could take 't' and 'f' to be 0-ary connectives, but
I do not actually do that in my own system. Rather, I take them as
defined 0-place predicate symbols. Thus, indeed the happy circumstance
is maintained that there is no formula that does not have a predicate
symbol in it (even if only a 0-place predicate symbol).
For a given language, I take an arbitrary sentence P (as short of one
as there is) in the language, then define:
t <-> (P -> P)
f <-> ~t.
However, in intuitionistic languages, I take 'f' as primitive. (As you
know, optional to take '~' as primitive instead.)
But, as to oxymoronic sounding terminology, we still have 'singulary
connective' such as '~'. I mean, 'connective' suggests connecting one
thing to another, but the negation symbol doesn>t connect one formula
with another as do the binary connectives.
MoeBlee |
|
| |
|
Back to top |
Balthasar Guest
|
Posted: Thu Jul 17, 2008 6:59 pm Post subject: Re: completeness what is it exactly |
|
|
On Wed, 16 Jul 2008 11:46:53 -0700 (PDT), MoeBlee <jazzmobe@hotmail.com>
wrote:
[quote]
And in pure propositional logic, there are no open formulas,
since there are no free variables anywhere, since there are
no [individual] variables at all.
What??? What do you call p, q, r, etc.?
I call them 'sentence letters'.
Yeah, also very common: "propositional variables".[/quote]
[quote]
In this context, by 'variable' we (I) mean 'individual variable'
(i.e., the ones used in predicate logic that are, e.g., free
or bound). Now, some authors also call sentence letters 'variables'.
But those are not the KIND of variables that are at stake when we
refer to 'free and bound'.
Right.[/quote]
[quote]
Ordinarily (there may be exceptions), an author takes a sentence
letter standing alone, or any formula built up from just sentence
letters and connectives to be a SENTENCE since it does not have
free variables (i.e., INDIVIDUAL variables that are not bound).
Moreover, as to what sentence letters are if they are not
considered variables of any kind, it is common to consider them
to be 0-place predicate symbols.
Right.[/quote]
But there>s a nice variant of propositional logic which allows to
quantify over propositions, i.e. there we would write
Ap(p -> p)
to express the theorem "id", etc. :-)
(Now the term "propositional variables" would actually be justified.)
In such a system FALSUM (_|_) could be defined:
_|_ =df Ap(p).
:-)
Moreover we also might define negation then:
~p =df p -> Aq(q) ,
or
~p =df p -> _|_.
:-)
[quote]
For example, the symbols of a propositional system may be categorized
as:
sentence letters: p q r, etc.
I>d propose to use uppercase letters in this case: P, Q, R, ...[/quote]
(And p, q, r, ... for "propositional variables". Yes, I know, it>s just
terminology, but...)
B.
P.S.
I hope I didn>t mix up things above (concerning quantified propositional
logic). |
|
| |
|
Back to top |
Balthasar Guest
|
Posted: Thu Jul 17, 2008 7:32 pm Post subject: Re: completeness what is it exactly |
|
|
On Wed, 16 Jul 2008 22:33:44 -0400, herbzet <herbzet@gmail.com> wrote:
[quote]
and we may regard 't' and 'f' (for 'truth' and 'falsehood') as 0-ary
connectives.
That>s new (to me) and amusing. We get the slightly odd-sounding
situation of wffs consisting of only connectives (e.g. 't v f')!
Yes. But actually its not that odd as it may seem at first:[/quote]
An n-ary connective takes n arguments [which are sentences] and results
in a sentence (then). For example, given the binary connective "&" and,
say, the sentence "P" and "Q", we get the sentence "P & Q".
Now in the "limit case" of n = 0, we have an 0-ary connective which
takes no (zero) arguments [which are sentences] and results in a
sentence (like any other n-ary connective). With other words, given the
0-ary connective "f" (or "t"), we get the sentence "f" (or "t") this
way. :-)
I guess, if we were more used to polish notation we would have less
problems with this idea.
There we FIRST write the n-ary connective, followed by its n arguments:
2-ary connectives:
Apq (p v q)
012
etc.
1-ary connectives:
Np (~p)
01
etc.
Hence in the case of 0-ary connectives F and T:
F
0
and
T
0
And we would write your formula the following way
ATF.
Makes sense (at least) to me.
A more realistic example:
ECpFNp. ((p -> f) <-> ~p)
B.
P.S. Polish notation also allows (in a natural, canonical way) for n-ary
connectives with n > 2. Clearly "infix notation" has a problem there. |
|
| |
|
Back to top |
Balthasar Guest
|
Posted: Thu Jul 17, 2008 7:55 pm Post subject: Re: completeness what is it exactly |
|
|
On Wed, 16 Jul 2008 20:57:27 -0700 (PDT), MoeBlee <jazzmobe@hotmail.com>
wrote:
[quote]
... by just taking the Lesniewski axioms (or is it Lukaciewz [sp]?
Lukasiewicz[/quote]
You should try to memorize his name. He gave propositional logic its
modern form.
[quote]
So I decided it was better anyway just to use an ordinary ~ -> system,
As Frege and later Lukasiewicz (simplifying Frege>s system) did.[/quote]
(Actually, Lukasiewicz & Tarski, btw.)
[quote]
for sake of not getting bogged down with axioms harder to intuit and
read. Also, using ~ -> makes my system more familiar to most readers
Right.[/quote]
You know that there>s a nice variant of this system, where "f" is a
primitive and "~" is defined.
A1 A -> (B -> A)
A2 (A -> (B -> A)) -> ((A -> B) -> (A -> C))
A3 ((A -> f) -> f) -> A
Def. ~A =df A -> f.
Hence A3 can (could) be reformulated the following way
A3' ~~A -> A.
Which highlights that this system embodies _classical_ propositional
logic. :-)
B.
Reference: A. Church, Introduction to Mathematical Logic I, 1956 |
|
| |
|
Back to top |
|