A carrier of statements equipped with a name sort, syntactic distinctness of names, and a substitution operation, characterized purely against a given mutual deducibility relation on the carrier — never against a basis’s own primitive relation. Distinctness is a syntactic side-condition some of the rules need, kept separate from any logical notion of identity.
(PF1) Statements and names are disjoint: taking them as two separate types, rather than two disjoint subsets of one shared type, gets this for free. (PF2) Substitution’s well-formedness (a substituted statement is again a statement, for any two names) is likewise automatic from substitution’s own type, a total function from a statement and two names to a statement.
The six primitive rules below (editors’ introduction, rules (6.1)–(6.6)) are transcribed directly against the source text’s own subscript/superscript pairing, \(a\binom{x}{y} = a[x := y]\).
substitution
structure Logic.Popper.HasSubstitution (Obj name : Type) (Mutual : Obj → Obj → Prop) : Type
Syntactic distinctness of two names.
DIST : name → name → Prop
(PF2). \(\mathrm{SUB}(a, x, y) = a[x := y]\): replace the name \(x\) by \(y\) in \(a\).
SUB : Obj → name → name → Obj
Freshness (PF3). Every statement has a name it does not depend on.
fresh : ∀ (a : Obj), ∃ x, Logic.Popper.NonDep Mutual (Logic.Popper.HasSubstitution.SUB Mutual) a x
(6.1). Substitution respects mutual deducibility.
sub_congr : ∀ {a b : Obj} (x y : name),
Mutual a b →
Mutual (Logic.Popper.HasSubstitution.SUB Mutual a x y)
(Logic.Popper.HasSubstitution.SUB Mutual b x y)(6.2). Substituting a name for itself does nothing.
sub_self : ∀ (a : Obj) (x : name), Mutual (Logic.Popper.HasSubstitution.SUB Mutual a x x) a
(6.3). For distinct \(x\) and \(y\): once \(x\) has been replaced by \(y\), \(x\) no longer occurs, so substituting anything for \(x\) again does nothing further.
sub_vacuous : ∀ (a : Obj) {x y : name} (z : name),
Logic.Popper.HasSubstitution.DIST Mutual x y →
Mutual
(Logic.Popper.HasSubstitution.SUB Mutual (Logic.Popper.HasSubstitution.SUB Mutual a x y) x z)
(Logic.Popper.HasSubstitution.SUB Mutual a x y)(6.4). Composition. Replacing \(x\) by \(y\) and then \(y\) by \(z\) agrees with replacing \(x\) by \(z\) and then \(y\) by \(z\): the trailing \(y\)-substitution on both sides folds in whatever \(y\) was already free in \(a\), so no distinctness or non-dependence hypothesis is needed.
sub_comp : ∀ (a : Obj) (x y z : name),
Mutual
(Logic.Popper.HasSubstitution.SUB Mutual (Logic.Popper.HasSubstitution.SUB Mutual a x y) y z)
(Logic.Popper.HasSubstitution.SUB Mutual (Logic.Popper.HasSubstitution.SUB Mutual a x z) y z)
(6.5). Two substitutions into the same name commute.
sub_comm_same : ∀ (a : Obj) (x y z : name),
Mutual
(Logic.Popper.HasSubstitution.SUB Mutual (Logic.Popper.HasSubstitution.SUB Mutual a x y) z y)
(Logic.Popper.HasSubstitution.SUB Mutual (Logic.Popper.HasSubstitution.SUB Mutual a z y) x y)
(6.6). Substitutions over pairwise-distinct names commute.
sub_comm : ∀ (a : Obj) {w x y z : name},
Logic.Popper.HasSubstitution.DIST Mutual w x →
Logic.Popper.HasSubstitution.DIST Mutual x z →
Logic.Popper.HasSubstitution.DIST Mutual z y →
Mutual
(Logic.Popper.HasSubstitution.SUB Mutual (Logic.Popper.HasSubstitution.SUB Mutual a x y) z
w)
(Logic.Popper.HasSubstitution.SUB Mutual (Logic.Popper.HasSubstitution.SUB Mutual a z w) x
y)
Show details
Outer dependencies: (none)