Proposition

Definition

A proposition is a statement that can be either true or false. In logic and mathematics, propositions are the basic units of reasoning and proof.

In Classical Logic

In classical logic, every proposition has exactly one of two truth values: true or false. Propositions can be combined using logical connectives:

• Conjunction: $P\wedge Q$ (P and Q)
• Disjunction: $P\vee Q$ (P or Q)
• Implication: $P\to Q$ (if P then Q)
• Negation: $\neg P$ (not P)

In Type Theory

Under the Curry-Howard correspondence, propositions correspond to types:

• A proposition $P$ is represented by a type
• A proof of $P$ is an element of that type
• $P$ is true if the type is inhabited (has at least one element)
• $P$ is false if the type is empty

This is known as propositions as types or the Brouwer-Heyting-Kolmogorov interpretation.

Examples

• $2+2=4$: A true proposition
• $3>5$: A false proposition
• $\forall n:\mathbb{N}.n+0=n$: A universally quantified proposition
• $\exists x:\mathbb{R}.x^2=2$: An existentially quantified proposition

Propositional vs Predicative

• A proposition is a statement with a definite truth value
• A predicate is a function from values to propositions, such as $P(x)$ where $x$ ranges over some domain

Related Concepts

• Type Theory: Framework where propositions are types
• Proof: Evidence establishing the truth of a proposition
• Predicate: A family of propositions indexed by values
• Logical Connective: Operations combining propositions