Lambda the Ultimate

Erm, what you're calling "first order predicate logic" there is propositional logic (the system of logic where the atomic signs are propositional variables); and what you're calling "second order predicate logic" is actually first order logic. (Second order logic includes predicate variables, and quantification over them.)

...start counting from zero (e.g. array indexes). Okay, out of my math class for a month, and I've already forgotten 90% of what they learnt me. :-)

that can't be right because he also uses "proposition" for constructive logic (and predicate logic includes the law of the excluded middle, doesn't it?).

i think i'm mixing up the language used to write things down and the system used to prove whether things are true or false.

a "proposition" is a statement in a language (called "logic" ?), whose truth values can be found by various thingies (logic instances?) (approaches to logic?).

it seems that the language spans different kinds of logic. do you see my problem (or one of them)?

It's true that first order logic is call the propositional calculus, and when you add quantifiers you get the "predicate calculus". Still, the term "proposition" has a more general meaning (see my earlier message). It sohuld be pretty clear from the context whether the distinction between the propositional calculus and the predicate calculus is relevant. It probably isn't.

...can be proven True or False. The propositional logic being the operators we can use to manipulate those statements. Propositions would be the p & q terms. p might be something like:

• Today is Friday
• It is raining
• The sun is hot

• Chris is good looking
• LtU is the best weblog in existence

Edit Note: Since we are delving into metaphysics, the the existential question is how do we know anything to be objectively True or False. That's a rabit hole that can lead one asunder. Mostly we have to deal with assumptions of what is true or false, and only test those assumptions if it helps us in a more pragmatic fashion.

yeah, thanks. got it now i think (i'm going to stop saying thank-you to everyone - please just assume it...)

Proposition being a statement that can be proven True or False.

No, that's wrong. Proposition is a semantic concept, not a proof-theoretic one; an unprovable statement can be true or false. For example, Gödel incompleteness theorems establish that for every axiomatization of arithmetic, there is some true proposition that the system can't prove.

I think your comments on "opinion" are also off the mark. Declarative statements like "Chris is good looking" and "LtU is the best weblog in existence" express propositions; whatever proposition "Chris is good looking" expresses in a given context, it has to be the case that "It is not the case that Chris is good looking" would be its negation in the same context, and that the conjunction of those two would be a contradiction.

"It is not the case that Chris is good looking" would be its negation in the same context, and that the conjunction of those two would be a contradiction.

As for unprovable statements, if we can't prove a proposition as true or false, how can we know it is true or false? The proposition becomes an assumption within the closed system.

Even if both statements are at odds with each other, I can probably roust up opinions on both sides of the matter (though the negation would likely be in the overwhelming majority).

I'd have to get pretty deep into semantics and pragmatics to properly justify the claim I made, but essentially, the precise details of how I use the word "context" in what I say are really important.

As for unprovable statements, if we can't prove a proposition as true or false, how can we know it is true or false?

Read up on Gödel's theorems.

doesn't godel's theorem say (only) that such things exist? that's not the same as saying that you know whether a particular unprovable statement is true or false, is it? doesn't this get back to constructivism? - what chris says is ok if you don't accept the law of the excluded middle, as far as i can tell (but i'm obviously no expert on this!)

Gödel's proof begins by constructing a formal proof system for propositions about arithmetic. It then shows how the formal proof system can be reduced to arithmetic expressions (which can be viewed as writing a program for the proof system using arithmetic as the language). With this framework, a proposition about arithmetic can be framed, which expresses that the proof system is consistent.

The theorem demonstrates that if the proposition is true (i.e. if the proof system is consistent), then the proof system cannot prove it.

As for unprovable statements, if we can't prove a proposition as true or false, how can we know it is true or false?

Empirically. Although people don't use the same formal proof system as Gödel, they use more powerful logical methods all the time without having run into a contradiction.

that's not the same as saying that you know whether a particular unprovable statement is true or false, is it?

The incompleteness theorem does single out a particular unprovable statement.

The incompleteness theorem does single out a particular unprovable statement.

argh. you're right. ("this statement is not provable", more or less, right?). so now i'm confused about something else, but i'll sort it out myself. thanks.

i may as well go ahead anyway, since i guess i learn more by being wrong... you need the axiom of inifinty somewhere in godel's proof (i think you effectively get to "this is not provable" by enumerating all provable statements). that means that "this statement is not provable" cannot be constructed. so if you're using a constructivist logic (which is generally not done, but very much is done when you're talking about types as propositions, which is where i started with all this) then you cannot decide whether "this is not provable" is true or false. so part of what i said earlier was still correct, i think.

does that make sense? [edit] i guess that's what you were saying anyway, since you always have to use something "more powerful" to show that the unprovable statement is true.

[later] so i think my confusion was partly thinking that the law of the excluded middle and the axiom of infinity were related. i don't see any connection now, except that neither is used in constructivist logic (i believe). unfortunately i don't have my book on set theory with me. but i shall go and search the stanford encylopedia...

[even later] ok, so i think hilbert shows the connection at http://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm - scroll down to the discussion of alpha + 1 = 1 + alpha and its negation.

sorry, i'm using this place to sort out muddled private thoughts...

"The theorem demonstrates that if the proposition is true (i.e. if the proof system is consistent), then the proof system cannot prove it."

The proof does not rely on on the proposition being "true". It shows that if the theory is consistent, neither G nor ^G can be proven (where G is a Godel sentence).

A proposition is an atomic element (i.e. you are not allowed to read it in English). You can't prove a proposition true or false. You can assign truth values to them, but how you do it is not covered by logic.

"As for unprovable statements, if we can't prove a proposition as true or false, how can we know it is true or false? The proposition becomes an assumption within the closed system.
"

We may be able to prove them in another axiomatic system more powerful than the original incomplete one.

...i'd say that it qualifies as a "proposition", if the statement can be assigned a value of "true" or "false" - not dependent upon being able to prove it one way or the other.

(That's what I get for posting near the end of day on Friday. Well, hopefully, short of anything else, the responses back and forth shed a bit of light on the subject matter).

for every axiomatization of arithmetic, there is some true proposition that the system can't prove.

is this right? isn't it for some axiomatizations?

some of your statements seem to assume a certain approach to logic and others seem to be more general and i'm having a hard time working out which is which...

Infinity--more precisely the axiom of infinity--stalks every page. This axiom says that the collection of all natural numbers exists as a set, on a par with all other sets. It is a very convenient axiom, and almost no practicing mathematician hesitates to use it. But it is not indispensable, as Kronecker and Brouwer, the fathers of intuitionism, correctly saw. The so-called constructivists (who are the modern intuitionists and who generally wear the mantle only part time) have effectively shown that all modern mathematics, including measure theory(!) (but not logic itself) can be reconstructed without its aid. Therefore it is wrong for Deutsch to make heavy use of Gödel's theorem (which depends on the axiom of infinity) to reach such conclusions as "Mathematicians [have made the mistake of thinking] that mathematical knowledge is more certain than other forms of knowledge." "Mathematical knowledge may, just like our scientific knowledge, be deep and broad, it may be subtle and wonderfully explanatory, it may be uncontroversially accepted; but it cannot be certain." The fact is that Gödel's examples of true theorems that cannot be proved within the framework of the standard axioms (or extensions thereof) always differ in fundamental ways from the bulk of the theorems that excite mathematicians' interest.

from http://naturalscience.com/ns/books/book02.html

(and is the "but not logic itself" related to the excluded middle?)

for every axiomatization of arithmetic...
Let your axioms be the set of true propositions of arithmetic and don't bother with any derivation rules.

Actually, Godel showed that for any reasonable set of axioms of arithmetics, there are statements S that both S and its negation are not provable. He did not use the notion of truth in his proof. Your "there is some true proposition that the system can't prove" is a consequence of his proof.

not directly related to what i was asking, but "it is raining" is actually used as an example, in one of oleg's links, to show why propositions in the sense of "the meaning of an expression in natural language" are not that useful - you can't reify (i hope i've used that fancy word correctly) them without qualifications (it might only be raining in one place at one time, for example).

(and it this sense that the wikipedia artical was emphasising, hence, partly, my confusion)

No, the classic (in the field of natural language semantics and pragmatics, 1970's or so) answer to that is to analyze the meaning of natural language statements as functions from contexts to propositions. The sentence She saw him is only true relative to a context, which provides the reference for the pronouns and the temporal indexes for the tense operator.

Long, long topic...

what does the "no" at the start of the title in the post above mean?

isn't that the aristotelian meaning in the wikipedia article (that i quoted)?

it seems to be more or less synonymous with assertion, but if this is the common use in "mathematical logic" as opposed to "philosophical logic" then wikipedia should be less dismissive.

The Aristotelian concept you cite makes use of the terms "subject" and "predicate"; i.e., it assumes that propositions all have a subject-predicate form. This is a defining assumption of Aristotelian logic, but one that modern logic rejects.

A proposition is simply anything that has (or can have) a truth value; most of the time there's no need to be any more precise about the concept than that. In extensional type theory, propositions simply are the members of the type t, which is the same thing as the boolean type. (Intensional logic is another story, but you probably don't need to go into that.)

ok, thanks. i've just re-read the article and suddently it seems a lot clearer, so i think that (and everyone else) helped.

from the article:

Often propositions are related to closed sentences, to distinguish them from what is expressed by an open sentence, or predicate. In this sense, propositions are statements that are either true or false. This conception of a proposition was supported by the philosophical school of logical positivism.

which i think is the sense people are arguing for here (i like the open/closed bit - i was about to say "ok, so is a proposition a predicate applied to something?")

wow. thanks. much clearer (or much clearer in admitting that it is less clear, if you see what i mean!)

From a pragmatic point of view there are two types of propositions: analytic and synthetic. An analytic proposition is one that can be proved given a certain set of rules and facts. Analytic truth is independent of time in so far as time is not considered. The analytic is often considered to be always true. Always was true and always will be true. This is probably a bit of a stretch. Actually analytic truth is a property of a set of rules and facts, nothing more.

A synthetic fact is one that is "perceived" to be true. This implies that a certain analytic system is used to parse a certain environment at a certain time. The systhetic fact is true at that time for that environment.

About any "Foundations of Mathematics" book will do. Most of the time, the books will have something like "Bridge to Advanced Mathematics" or "Translation to Advanced Mathematics." I cannot find one online but I have a couple of books here in my office. I could send you "Bridge to Abstract Mathematics" by Ronald P. Morash if you wish. I like and use "Introduction to Advanced Mathematics Second Edition" by William Barnier and Norman Feldman for my "Foundations of Mathematics" class.

ok, thnaks. i'll have a look both online and at my old maths books - it's quite possible there's something there (i didn't think to look - i studied physics and am not sure how deep the maths textbooks i have go)

In propositinal calculus, 'sentence' and 'proposition' are usually interchangeable. In predicate calculus, 'sentence' is a synonym of the 'closed formula'.

I think you are quite right about propositions, at least that's more or less what I've been taught too.

I guess in a PL-context, the closest thing to a "proposition" would be something like an algorithm, that can be implemented in any language, while a "sentence" would be a concrete program that implements an algorithm. Funny thing is, there's no (general) way to determine whether two programs "do the same thing" or not (i.e. a "propositional" identity criterion) either...

I agree that the distinction between algorithm and code is very like the distinction between proposition and sentence.