[Haskell-cafe] In what language...?

[Benedict Eastaugh]

On 26 October 2010 20:43, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
>
>> Propositional logic is quite a simple logic, where the building blocks
>> are atomic formulae and the usual logical connectives. An example of a
>> well-formed formula might be "P → Q". It tends to be the first system
>> taught to undergraduates, while the second is usually the first-order
>> predicate calculus, which introduces predicates and quantifiers.
>
> Already I'm feeling slightly lost. (What does the arrow denote? What's are
> "the usual logcal connectives"?)

The arrow is just standard logical notation for the conditional: "if
... then" in English. If you were to read "P → Q" aloud, it would
sound like "If P then Q". It's one of the usual logical connectives I
mentioned.

The others are "∧" (conjunction; "and", in English); "∨" (disjunction;
"or". Note that it's inclusive: if both operands are true then the
whole expression is true. This is different to how the word "or"
functions in everyday English, where it's exclusive: you can have
cheesecake or apple pie, but not both); "¬" (negation; "not"--the only
unary operator in the usual group of connectives) and "↔"
(biconditional; "if and only if").

They are the usual logical connectives purely in virtue of the fact
that they're the ones we tend to use most of the time. Historically
speaking this is because they seem to map well onto use cases in
natural language.

However, there are many other possible logical connectives; I have
only mentioned a few unary and binary connectives. There are 4 unary
operators, 16 binary operators, 256 ternary operators, and in general,
2 ^ 2 ^ n logical connectives for n < ω (i.e. the first infinite
ordinal: we only consider operators with a finite number of operands).

We could write the four unary operators quite easily in Haskell,
assuming that we take them as functions from Bool to Bool:

> data Bool = True | False
>
> not :: Bool -> Bool
> not True = False
> not False = True
>
> id :: Bool -> Bool
> id True = True
> id False = False
>
> true :: Bool -> Bool
> true _ = True
>
> false :: Bool -> Bool
> false _ = False

The `true` and `false` functions are constant functions: they always
produce the same output regardless of their inputs. For this reason
they're not very interesting. The `id` function's output is always
identical to its input, so again it's not very interesting. The `not`
function is the only one which looks like it holds any interest,
producing the negation of its input. Given this it shouldn't surprise
us that it's the one which actually gets used in formal languages.

>> Predicates are usually interpreted as properties; we might write
>> "P(x)" or "Px" to indicate that object x has the property P.
>
> Right. So a proposition is a statement which may or may not be true, while a
> predicate is some property that an object may or may not possess?

Exactly. The sentence "There is a black beetle" could be taken to
express the proposition that there is a black beetle. It includes the
predicates "is black" and "is a beetle". We might write this in
first-order logic, to make the predicates (and the quantification)
more explicit, as "∃x [Black(x) ∧ Beetle(x)]". I.e., "There exists
something that is black and is a beetle".

I hedged, saying that we usually interpret predicates as properties,
because the meaning of an expression in a formal language (or, indeed,
any language) depends on the interpretation of that language, which
assigns meanings to the symbols and truth-values to its sentences.

Benedict.