What is a Proposition?

I just started reading "Type Theory and Functional Programming" and realised pretty rapidly that I wasn't sure what a proposition was.

When I look at Wikipedia - http://en.wikipedia.org/wiki/Proposition - they seemed rather negative on the whole idea. If propositions are questionable how can you do something as concrete as write programs with them?

Am I just getting two different meanings of "proposition" mixed up? In the article it says

In Aristotelian logic a proposition is a particular kind of sentence: one which affirms or denies a predicate of a subject.

Even I know what a predicate is, so should I just run with this definition?


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

First and Second Order Predicate Logic?

First order predicate logic being those statements that are either true or false, with propositions such as:

  • p
  • ¬p (not p)
  • p ∧ q (p and q)
  • p ∨ q (p or q)
  • p → q (p implies q, if p then q)

From these we can extrapolate further propositions and tautologies such as:

  • p ↔ q (biconditional (p → q) ^ (q → p))
  • p ⊕ q (exclusive or (p ∨ q) ^ ¬(p ^ q))
  • ¬(p ∧ q) ≡ ¬p ∨ ¬q
  • ¬(p &or q) ≡ ¬p ∧ ¬q (De Morgan's laws)

And many other extrapolations that I had to derive/memorize for my recent graduate course in Discrete Mathematics.

Second order predicate logic would deal in quantifiers such as:

  • ∀xP(x) (universal quantifier: forall x, P(x) is true)
  • ∃xP(x) (existential quantifier: there exists an element x such thaty P(x) is true).

And from, these you do further combinations and extrapolations. Anyhow, that's what I consider to be the Propositional Calculus (aka Logic). Though the math on it can go quite deep, it starts out fairly simple and builds from there.

No, that's wrong.

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.)

Never could get the hang of PL's that....

...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. :-)

so a proposition is just a "s

so a proposition is just a "sentence" in first order predicate logic?

(ps i am impressed by your html symbol skills!)

that can't be right because h

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 lo

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.

Proposition being a statement that...

...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
There are propositions which are not in the category of True or False:

  • Chris is good looking
  • LtU is the best weblog in existence
These would involve matters of opinion and can not be quantitatively proven or disproven. With the first kind of propositions, one can use the predicate logic to come up with an approach that can express anything that can be expressed in the lambda calculus (or by a Turing machine). Not that the expression will be concise, but it is theoretically possible to map the predicate calculus to and from the lambda calculus.

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 t

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

No, that's wrong too.

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.

The paradox....

"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.

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).

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 a

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 (

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!)

incompleteness theorem

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 do

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

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

"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).

Not according to my source

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

"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.

After further consideration...

...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 a

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

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

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

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 sta

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

Philosophy or Math?

Usually "proposition" simply means a declarative sentence. Usually the term is used to refer to the meaning of the sentence (though what "meaning" is can be quite subtle).

For most practical matters (i.e., when doing real math and logic), a precise definition of this term isn't that important, when it refers to natural language sentencse, rather than to well formed formulas inside the formal system.

So I wouldn't worry about it too much. If you want to explore a bit more, you might want to skim over this paper.

P.S It's great to see a thread started by the second member of LtU, with an answer by the third member! On the Net such continuity is quite amazing...

isn't that the aristotelian m

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

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-rea

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?")

See Stanford Encyclopedia of Philosophy

I believe questions like that are best answered by the Stanford Encyclopedia of Philosophy. It, unlike Wikipedia, is authoritative, and is of the supreme quality. For the question at hand, please see these entries




For programming languages (logic programming), the following article is quite relevant:

Perhaps the Stanford Encyclopedia should be mentioned more prominently on LtU?

wow. thanks. much clearer (

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

The Internet...

... is surprisingly full of mathematics textbooks. Check out this one that covers propositional & predicate logic and more...

According to that text, a proposition is an atomic sentence that cannot be deconstructed (heh) any further by using any logic tools. It could be "The moon is made of cheese".

Article by Per Martin-Löf

The article " On the Meanings of the Logical Constants and the Justifications of the Logical Laws" (actually a transcript of a series of three lectures) by Per Martin-Löf starts with an extended discussion of the history and current use of the word "proposition"

I like to think of analytic l

I like to think of analytic logic and propositions as consisting of things that we choose to be part of our analytic conception of reality. Such things form a system in which everything is linked mathematically or logically. One proposition can be derived from the others and there is no contradiction. Everything is either true or false.

But this is not what we actually experience as we move through time. There are many existant things that are not analytic but might become so in a new context. Science is about experiment and experience as well as math and logic. The propositions we choose at any time are always a pragmatic choice, chosen to make sense out of the world and to bring order to our existence.

Pragmatically speaking

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.

Model theory perspective

In the context of a formal language, you are going to need an interpretation to say what your language means. Propositions are the elements of the formal language that get mapped into the set {true, false} in every interpretation.

If you wanted a probability calculus instead of a logical calculus you would not want your propositions to be either true or false, you would want some notion of how likely they are, so you might try mapping them into the set [0,1]. I think that particular choice is useless because it cannot handle correlations.

You could go for a fuzzy logic; you could again use [0,1] as your range, this time as a pragmatic bodge where you say TALL=0.8 to say that some-one is quite tall, conflating the issue of how tall with the issue of how sure we are that he is tall.

Saying that X is a proposition is simply a way of saying that we are not going to concern ourselves with worries that X might be uncertain, or a matter degree.

intro to logic

can anyone suggest a good simple intro to logic? just the normal boolean kind (excluded middle, bivalent). i want to be able to prove things without using truth tables (preferably with lots of horizontal lines as that's how ttfp does it).

background - i'm doing the exercises in ttfp and i ended up convincing myself that i needed an extra axiom. turns out it was the law of non-contradiction which some guy called aristotle dreamt up, so i'm thinking that maybe i need a bit more background...


ps interesting article (not related to programming languages though) - http://plato.stanford.edu/entries/dialetheism/

About any "Foundations of

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

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)

Propositions and identity

Propositions are almost the same thing as sentences: propositions are what you might know, or claim or be the case, but the reason that philosophers have problems with propositions that they don't have with sentences si that they want them to have a well-defined notion of identity: they want to say that "It is raining" in English expresses the same proposition as "Es regnet" expresses in German, even though they are quite different sentences. All kinds of ways of determining what it is that is the same in these two cases have been made, the most popular is truth-conditions.

Mathematical logicians don't tend to care about the difference between propositions and sentences, so what Ehud says: that you can treat propositions as being sentences, is right when you are formal enough.

propositions and sentences

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

Analogy in PLs

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.

I'm sorry

I've been resisting this comment for weeks now- hoping that it'll fall off the active list. Unfortunately, I am no longer able to resist.

What is a proposition? "Hey, baby- wanna party?"

My apologies. I'll shut up now.