Profound–Intuitionistic

Seminar on Proof Representations (Dagstuhl 2024)

State your conjecture...

...

...

i.e.,

|

… or try one of these:

Propositional

Structural

a \to a (initial)
a \to b \to a (weakening)
a \to a \and a (contraction)

Connectives

a \and b \to a \and b
a \and b \to a
a \and b \to b
a \and b \to (a \to b \to c) \to c
a \to \top
(\top \to c) \to c
a \to a \or b
b \to a \or b
a \or b \to (a \to c) \to (b \to c) \to c
\bot \to c
a \or b \to b \or a
a \and b \to b \and a
(a \to b) \to ((b \to \bot) \to a \to \bot)

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
(a \to b) \or (b \to a) (not provable)
(((a \to b) \or (b \to a)) \to \bot) \to \bot

First-Order

(\A [x, y] p (g x y)) \to \A [z] p (g z z)
p k \to \E [x] p x
(\E [x] p x) \to (\A [z] (p z \to c)) \to c
(\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))
((\A [x] p x) \or c) \to \A [x] (p x \or c)
((\A [x] p x) \to c) \to \E [x] (p x \to c) (not provable)
((\E [x] p x) \or c) \to \E [x] (p x \or c) (not provable)

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 \A or \E, i.e., they can be written \A [x] or \E [x]. When unambiguous, the types will be inferred.
The connectives \and, \or, \to are 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 \eq cannot be written infix. This may be fixed with a hand-written LR parser in the future.