State your conjecture...
i.e.,
|
… or try one of these:
Propositional
- a \to \top
- a \to a
- a \to b \to a
- a \to a \and a
- a \and b \to b \and a
- a \to b \to b \and a
- (a \to b \to c) \to (a \to b) \to a \to c
Classically valid formulas (and their double negations)
- a \or (a \to \bot)
(not provable) - ((a \or (a \to \bot)) \to \bot) \to \bot
- ((a \to b) \to a) \to a
(not provable) - ((((a \to b) \to a) \to a) \to \bot) \to \bot
Instantiation
- \A [x, y] p (g x y) \to p (g x x)
(not provable) - p j \to \E [x] p x
- (\A [x] p x) \to p k
- (\E [x] p x \and (p x \to \bot)) \to \bot
- (\A [x] \E [y] r x y) \to (\E [w] \A [z] r z w)
(not provable) - (\E [w] \A [z] r z w) \to (\A [x] \E [y] r x y)
- (\A [x] p x) \to \E [y] p y
(not provable) - (\A [x] p x) \to \A [y] p y
- (\A [x] p x \to p (f x)) \to p j \to p (f (f j))
Guide
Concrete Syntax for Signatures
- Basic types have the signature type
\type - Predicates have types built with the type
constructor
->with the target type\o - Term constants have types built with the infix type
constructor
-> ->is right-associative
Concrete Syntax for Formulas
| to get | write |
|---|---|
| \eq j k | \eq j k |
| a \and b | a \and b or a & b |
| \top | \top or #t |
| a \or b | a \or b or a | b |
| \bot | \bot or #f |
| a \to b | a \to b or a => b |
| \A [x] p x | \A [x:i] p x |
| \E [x] p x | \E [x:i] p x |
| [x] f x | [x] f x |
- Types can often be omitted after the variable in
\Aor\E, i.e., they can be written\A [x]or\E [x]. When unambiguous, the types will be inferred. - The
connectives
\and,\or,\toare right-associative and listed in the order of decreasing precedence. - Both
\A [x:i]and\E [x:i]behave like prefix connectives of the lowest precedence. - Due to an ambiguity in the LALR grammar, equality
\eqcannot be written infix. This may be fixed with a hand-written LR parser in the future.