Dane Sabo
ae0ab17291
R "Zettelkasten/Hub Notes/NNFM Ontology.canvas" -> "NNFM Ontology.canvas" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Assembly/Assembly Canvas.canvas" -> "Programming/Assembly/Assembly Canvas.canvas" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Assembly/Untitled.md" -> Programming/Assembly/Untitled.md R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/LEAN/Learning Plan.md" -> "Programming/Formal Methods/LEAN/Learning Plan.md" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/LEAN/Tutorial World.md" -> "Programming/Formal Methods/LEAN/Tutorial World.md" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/TLA/TLA Canvas.canvas" -> "Programming/Formal Methods/TLA/TLA Canvas.canvas" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/TLA/TLA+ Learning Plan.md" -> "Programming/Formal Methods/TLA/TLA+ Learning Plan.md" R "Zettelkasten/Hub Notes/Permanent Notes/Programming/Formal Methods/TLA/What is TLA?.md" -> "Programming/Formal Methods/TLA/What is TLA?.md"
64 lines
1.6 KiB
Markdown
64 lines
1.6 KiB
Markdown
---
|
|
id: 20250818132018
|
|
title: Predicate Logic
|
|
type: permanent
|
|
created: 2025-08-18T17:20:18Z
|
|
modified: 2025-08-18T20:20:03Z
|
|
tags: []
|
|
---
|
|
|
|
# Predicate Logic
|
|
|
|
Predicate logic extends propositional logic by using
|
|
predicates and quantifiers.
|
|
|
|
- **Predicates** express properties or relations (e.g.,
|
|
$Pump(x)$ or $Connected(v,c)$).
|
|
|
|
- **Quantifiers** let us say something about *all* or *some*
|
|
in the domain.
|
|
- $\forall$ = for all
|
|
- $\exists$ = exists, at least one
|
|
- $\exists!$ = there exists exactly one
|
|
|
|
Predicates kind of look like functions: $Pump(x)$ means $x$ is
|
|
a pump.
|
|
|
|
**Relational Predicates** have two inputs:
|
|
$Connected(x,y)$ means pump $x$ is connected to valve $y$
|
|
|
|
## Examples
|
|
|
|
Predicate logic requires you to *introduce the
|
|
variable first*. This feels weird at first, but is
|
|
mathematically explicit. The predicate does not define the
|
|
input, it only defines the property!
|
|
|
|
Here's an example:
|
|
|
|
$\forall x (Pump(x) \rightarrow Working(x))$
|
|
|
|
Means that 'every pump works'. But, we define first a set x,
|
|
then specify it is a pump for all x, and that they all of x,
|
|
which are all pumps, work.
|
|
|
|
What if we have one pump that doesn't work?
|
|
|
|
$\exists x(Pump(x) \wedge \neg Working(x))$
|
|
|
|
## Nested Qualifiers
|
|
|
|
We can stack qualifiers and do some nifty things.
|
|
How do we say: There exists one controller that stabilizes
|
|
every plant?
|
|
|
|
$ \exists k \forall G (Plant(G) \rightarrow Stabilizes(k,G))$
|
|
|
|
This is obviously not possible. So how do we say the
|
|
opposite, that for any plant there exists at least one
|
|
stabilizing controller:
|
|
|
|
$ \forall G \exists k (Plant(G) \rightarrow (Controller(k)
|
|
\wedge Stabilizes(k,G)))$
|
|
|