Commit 77748667 authored by Michael Kohlhase's avatar Michael Kohlhase

Merge branch 'devel' of https://gl.mathhub.info/MMT/LATIN2 into devel

parents a8ab02ca f3a10102
......@@ -2,7 +2,7 @@
<module type="JAVA_MODULE" version="4">
<component name="NewModuleRootManager">
<output url="file://$MODULE_DIR$/bin" />
<output-test url="file://$MODULE_DIR$/../../../github.com/UniFormal/MMT/src/out/test/LATIN2" />
<output-test url="file://$MODULE_DIR$/bin/out/test/LATIN2" />
<exclude-output />
<content url="file://$MODULE_DIR$">
<sourceFolder url="file://$MODULE_DIR$/export/lf-scala" isTestSource="false" />
......
namespace latin:/algebraic❚
fixmeta latin:/?SFOLEQND❚
theory AdditiveSet =
structure add : ?Set❙
theory AdditiveMagma =
include ?AdditiveSet❙
structure add : ?Magma =
include ?AdditiveSet/add❙
op # 1 + 2 prec 40❙
theory AdditiveCommutative =
include ?AdditiveMagma ❙
structure add : ?Commutative =
include ?AdditiveMagma/add❙
theory AdditiveIdempotent =
include ?AdditiveMagma ❙
structure add : ?Idempotent =
include ?AdditiveMagma/add❙
theory AdditiveSemigroup =
include ?AdditiveMagma❙
structure add : ?Semigroup =
include ?AdditiveMagma/add❙
theory AdditiveCommSemigroup =
include ?AdditiveSemigroup❙
include ?AdditiveCommutative❙
structure add : ?CommSemigroup =
include ?AdditiveSemigroup/add❙
include ?AdditiveCommutative/add❙
namespace latin:/
namespace latin:/algebraic
fixmeta ur:?LF
fixmeta powertypes?PowerSFOL
theory Generated =
include ☞latin:/powertypes?PowerSFOL
generate : {S} tm ℘S ⟶ tm ℘S ❘# ⟨ 2 ⟩ prec 10 ❙
generating : {S, A: tm ℘S} ⊦ A ⊆ ⟨A⟩
monotone : {S, A: tm ℘S, B: tm ℘S } ⊦ A ⊆ B ⟶ ⊦ ⟨ A ⟩ ⊆ ⟨ B ⟩
idempotent : {S, A: tm ℘S} ⊦ ⟨ ⟨ A ⟩ ⟩ ≐ ⟨A⟩ ❙
theory GeneratedSets =
include ?Set
structure generated : latin:/?ClosureOperator =
X = universe
closure # ⟨ 1 ⟩ prec 10
theory GeneratedMagmas =
include ?Magma❙
include ?GeneratedSets❙
closure_op: {S} ⊦ ∀[x]∀[y] x∈⟨S⟩ ⇒ y∈⟨S⟩ ⇒ (x∘y)∈⟨S⟩❙
theory GeneratedPointed =
include ?Pointed❙
include ?GeneratedMagmas❙
closure_elem: {S} ⊦ e∈⟨S⟩❙
theory GeneratedInverseFun =
include ?InverseFun❙
include ?GeneratedPointed❙
closure_inv: {S} ⊦ ∀[x] x∈⟨S⟩ ⇒ x⁻∈⟨S⟩❙
\ No newline at end of file
......@@ -2,6 +2,40 @@ namespace latin:/algebraic❚
fixmeta latin:/?SFOLEQ ❚
theory Quasigroup =
include ?Magma ❙
div_left : ⊦ ∀[x] ∀[y] ∃[a] (a∘x ≐ y) ❙
div_right: ⊦ ∀[x] ∀[y] ∃[b] (x∘b ≐ y) ❙
theory Loop =
include ?Quasigroup ❙
include ?Monoid❙
theory InverseFun =
include ?Monoid❙
inv : U ⟶ U❘# 1 ⁻ prec 60❙
inverseLeft: ⊦ ∀[x] x⁻∘x ≐ e❙
inverseRight: ⊦ ∀[x] x∘x⁻ ≐ e❙
div : U ⟶ U ⟶ U❘= [x,y]x∘y⁻❙
invL : {x} ⊦ x⁻∘x≐e❘= [x] inverseLeft forallE x❙
invR : {x} ⊦ x∘x⁻≐e❘= [x] inverseRight forallE x❙
inverse_inv : {x} ⊦ inverse x (x⁻)❘= [x] andI invR invL❙
inv_unit : ⊦ e⁻≐e❘ = inverse_unique inverse_inv inverse_neutral❙
inv_op : {x,y} ⊦ (x∘y)⁻ ≐ y⁻∘x⁻❘
= [x,y] inverse_unique inverse_inv (inverse_op inverse_inv inverse_inv)❙
theory InverseExistence =
include ?Monoid ❙
inverseLeft: ⊦ ∀[x]∃[i] i∘x ≐ e ❙
inverseRight: ⊦ ∀[x]∃[i] x∘i ≐ e ❙
theory Group =
include ?Monoid ❙
include ?InverseFun ❙
......@@ -9,11 +43,7 @@ theory Group =
theory CommGroup =
include ?Group❙
include ?Commutative❙
zero = e ❘# O ❙
add = op ❘# 1 + 2 prec 70 ❙
minus = inv ❘# -1 prec 40 ❙
sub = [x,y] op x (inv y) ❘# 1 - 2 prec 70 ❙
include ?CommMonoid❙
theory GroupHom =
......@@ -26,4 +56,3 @@ theory GroupHom =
// e: ⊦ U domain/e ≐ codomain/e ❙
\ No newline at end of file
namespace latin:/algebraic❚
fixmeta latin:/?SFOLEQLFXI
fixmeta latin:/?SFOLEQND
theory Set =
universe : tp❙
U = tm universe❙
theory Hom =
structure domain : ?Set =
structure codomain : ?Set =
theory SetHom =
structure domain : ?Set❚
structure codomain : ?Set❚
U : domain/U ⟶ codomain/U ❙
theory Magma =
include ?Set ❙
op : U ⟶ U ⟶ U ❘# 1 ∘ 2 prec 50 ❙
op : U ⟶ U ⟶ U ❘# 1 ∘ 2 prec 50❙
total structure divisibility : ?Relation =
include ?Set❙
rel = [x,z] ∃[y]x∘y≐z❙
theory MagmaHom =
include ?Hom ❙
include ?SetHom ❙
structure domain : ?Magma =
U = domain/U
include ?SetHom/domain
structure codomain : ?Magma =
U = codomain/U
include ?SetHom/codomain
op : ⊦ ∀[x]∀[y] U (domain/op x y) ≐ codomain/op (U x) (U y) ❙
op : ⊦ ∀[x]∀[y] U (x domain/∘ y) ≐ U x codomain/∘ U y ❙
theory SubSet =
structure parent : ?Set =
U # P❙
universe : P ⟶ prop❘# U 1 prec 40❙
theory SubMagma =
include ☞latin:/?TypedLogic
include ?SubSet
structure parent : ?Magma =
universe # parent_universe ❙
U # parent_U ❙
include ?SubSet/parent❙
universe : tm parent_universe ⟶ prop ❙
op: ⊦ ∀[x]∀[y] universe x ⇒ universe y ⇒ universe (x ∘ y) ❙
op: ⊦ ∀[x]∀[y] U x ⇒ U y ⇒ U (x parent/∘ y) ❙
theory Commutative =
......@@ -55,7 +62,7 @@ view OppositeMagma : ?Magma → ?Magma =
theory Idempotent =
include ?Magma ❙
idem: ⊦ ∀[x] (x ∘ x) ≐ x ❙
idem: ⊦ ∀[x] x∘x ≐ x ❙
view OppositeCommMagma : ?Commutative → ?Commutative =
......@@ -64,49 +71,88 @@ view OppositeCommMagma : ?Commutative → ?Commutative =
comm = comm ❙
theory PowerAssociative =
include ?Magma ❙
power_assoc : ⊦ ∀[x] (x∘x)∘x ≐ x∘(x∘x)❙
theory Semigroup =
include ?Magma ❙
assoc : ⊦ ∀[x]∀[y]∀[z] (x∘y)∘z ≐ x∘(y∘z)
assoc_ax : ⊦ ∀[x]∀[y]∀[z] (x∘y)∘z ≐ x∘(y∘z)
assoc: {x,y,z} ⊦ (x∘y)∘z ≐ x∘(y∘z)❘
= [x,y,z] assoc_ax forallE x forallE y forallE z❙
assocR: {x,y,z} ⊦ x∘(y∘z) ≐ (x∘y)∘z❘
= [x,y,z] assoc sym❙
assoc4: {w,x,y,z} ⊦ ((w∘x)∘y)∘z ≐ w∘(x∘(y∘z))❘
= [w,x,y,z] trans3 (assoc congT [u]u∘z) assoc (assoc congT [u]w∘u)❙
assoc4R: {w,x,y,z} ⊦ w∘(x∘(y∘z)) ≐ ((w∘x)∘y)∘z❘
= [w,x,y,z] assoc4 sym❙
assoc5: {v,w,x,y,z} ⊦ (((v∘w)∘x)∘y)∘z ≐ v∘(w∘(x∘(y∘z)))❘
= [v,w,x,y,z] trans4 (assoc4 congT [u]u∘z) assoc
(assoc congT [u]v∘u) (assoc congT [u]v∘(w∘u))❙
// from a previous version of magmas.mmt
// assocR: {x,y,z} x∘(y∘z) = (x∘y)∘z❘
// = [x,y,z] sym assoc❙
// assoc4: {w,x,y,z} ((w∘x)∘y)∘z = w∘(x∘(y∘z))❘
// = [w,x,y,z] trans3 (assoc congT [u]u∘z) assoc (assoc congT [u]w∘u)❙
// assoc4R: {w,x,y,z} w∘(x∘(y∘z)) = ((w∘x)∘y)∘z❘
// = [w,x,y,z] sym assoc4❙
// assoc5: {v,w,x,y,z} (((v∘w)∘x)∘y)∘z = v∘(w∘(x∘(y∘z)))❘
// = [v,w,x,y,z] trans4 (assoc4 congT [u]u∘z) assoc
// (assoc congT [u]v∘u) (assoc congT [u]v∘(w∘u))❙
realize ?PowerAssociative❙
power_assoc = forallI [x] assoc❙
// total structure divisibility : ?Transitivity =
include ?Magma/divisibility❙
// metarel/trans = [x,y,z,p,q] p existsE [xy,xyP] q existsE [yz,yzP]
existsI (xy ∘ yz) trans3 assocR (xyP congT [u]u∘yz) yzP❙
// ❚
view OppositeSemigroup : ?Semigroup → ?Semigroup =
include ?OppositeMagma ❙
op = op ❙
assoc = assoc
assoc_ax = assoc_ax
theory CommSemigroup =
include ?Semigroup ❙
include ?Commutative ❙
theory Band =
include ?Semigroup ❙
include ?Idempotent ❙
theory CommIdempotent =
include ?Idempotent❙
include ?Commutative❙
theory Semilattice =
include ?CommSemigroup❙
include ?Band❙
include ?CommIdempotent❙
theory Pointed =
include ?Set❙
elem : U ❘# e
elem : U❙
theory RightUnital =
theory UnitElement =
include ?Magma❙
include ?Pointed❙
neutralR : ⊦ ∀[x] x∘e ≐ x ❙
structure unitelem : ?Pointed =
include ?Set❙
elem # e❙
involution : U ⟶ prop❘ = [x] x∘x≐e❙
theory RightUnital =
include ?UnitElement❙
neutralR : ⊦ ∀[x] x∘e ≐ x❘role Simplify❙
neutR: {x} ⊦ x∘e≐x❘= [x] neutralR forallE x❙
theory LeftUnital =
include ?Magma
include ?Pointed
neutralL : ⊦ ∀[x] e∘x ≐ x ❙
include ?UnitElement
neutralL : ⊦ ∀[x] e∘x ≐ x❘ role Simplify
neutL: {x} ⊦ e∘x≐x❘= [x] neutralL forallE x❙
theory Unital =
......@@ -114,66 +160,85 @@ theory Unital =
include ?RightUnital ❙
theory Monoid =
include ☞latin:/?NatInduct ❙
include ?Semigroup ❙
include ?Unital ❙
inductive_definition auxpow(a : U) : nat() ❘=
n : type ❘= U ❙
z : n ❘= e ❙
s : n ⟶ n ❘= [m : U] a ∘ m ❙
theory AbsorbingElement =
include ?Magma❙
structure absorbingelem : ?Pointed =
include ?Set❙
elem # abs❙
pow: U ⟶ nat/n ⟶ U ❘= auxpow/n ❘# 1 ^ 2 ❙
theory RightAbsorptive =
include ?AbsorbingElement❙
absorbR : ⊦ ∀[x] x∘abs ≐ abs❘role Simplify❙
theory IdempotentMonoid =
include ?Idempotent
include ?Monoid
theory LeftAbsorptive =
include ?AbsorbingElement
absorbL : ⊦ ∀[x] abs∘x ≐ abs❘role Simplify
theory CommMonoid =
include ?Commutative❙
include ?Monoid
theory Absorptive =
include ?LeftAbsorptive❙
include ?RightAbsorptive
theory Quasigroup =
include ?Magma ❙
div_left : ⊦ ∀[x] ∀[y] ∃[a] (a∘x ≐ y) ❙
div_right: ⊦ ∀[x] ∀[y] ∃[b] (x∘b ≐ y) ❙
theory Powers =
include ?PowerAssociative❙
include ?Unital❙
include ☞latin:/?Nat❙
power : U ⟶ ℕ ⟶ U❘# 1 ^ 2 prec 60❙
power_zero: {x} ⊦ x^0 ≐ e❘ role Simplify❙
power_succ: {x,n} ⊦ x^(n') ≐ x^n∘x❘ role Simplify❙
theory Band =
include ?Idempotent ❙
include ?Semigroup ❙
theory Monoid =
include ?Semigroup❙
include ?Unital❙
inverse : U ⟶ U ⟶ prop❘ = [x,xˈ] x∘xˈ≐e ∧ xˈ∘x≐e❘# inverse 1 2 prec 30❙
inverse_sym : {x,xˈ} ⊦ inverse x xˈ ⟶ ⊦ inverse xˈ x❘
= [x,xˈ,p] andI (p andEr) (p andEl)❙
inverse_unique : {x,x1,x2} ⊦ inverse x x1 ⟶ ⊦ inverse x x2 ⟶ ⊦ x1≐x2❘
= [x,x1,x2,p,q] trans3
((neutR sym) trans (q andEl sym congT [u]x1∘u))
assocR
((p andEr congT [u]u∘x2) trans neutL)❙
inverse_neutral : ⊦ inverse e e❘
= andI neutL neutL❙
inverse_op : {x,y,xˈ,yˈ} ⊦ inverse x xˈ ⟶ ⊦ inverse y yˈ ⟶ ⊦ inverse (x∘y) (yˈ∘xˈ)❘
= [x,y,xˈ,yˈ,p,q] andI
(trans3 assoc ((trans3 assocR (q andEl congT [u]u∘xˈ) neutL) congT [u]x∘u) (p andEl))
(trans3 assoc ((trans3 assocR (p andEr congT [u]u∘y) neutL) congT [u]yˈ∘u) (q andEr))
involution_inverse: {x} ⊦ involution x ⇔ inverse x x❘
= [x] equivI ([p] andI p p) ([p] p andEl)❙
theory Loop =
include ?Quasigroup ❙
theory Involutory =
include ?Monoid❙
involutory: {x} ⊦ involution x❙
inverse_refl : {x} ⊦ inverse x x❘
= [x] involution_inverse equivEl involutory❙
inverse_ident : {x,y} ⊦ inverse x y ⟶ ⊦ x≐y❘
= [x,y,p] inverse_unique inverse_refl p❙
theory InverseFun =
theory IdempotentMonoid =
include ?Monoid❙
inv : U ⟶ U❘# 1 ⁻ prec 60❙
inverseLeft: ⊦ ∀[x] x⁻∘x ≐ e❙
inverseRight: ⊦ ∀[x] x∘x⁻ ≐ e❙
include ?Band❙
theory Semilattice =
include ?Semigroup
include ?Idempotent
theory CommMonoid =
include ?Monoid
include ?CommSemigroup
theory BoundedSemilattice =
include ?Semilattice ❙
include ?CommMonoid ❙
theory InverseExistence =
include ?Monoid ❙
inverseLeft: ⊦ ∀[x]∃[i] i∘x ≐ e ❙
inverseRight: ⊦ ∀[x]∃[i] x∘i ≐ e ❙
namespace latin:/algebraic❚
fixmeta latin:/?SFOLEQND❚
theory Relation =
include ?Set❙
rel : U ⟶ U ⟶ prop❘# 1 $ 2 prec 30❙
structure metarel : latin:/?Relation =
carrier = U❙
rel = [x,y] ⊦ x $ y❙
theory Reflexivity =
include ?Relation❙
structure metarel : latin:/?Reflexivity =
include ?Relation/metarel❙
theory Symmetry =
include ?Relation❙
structure metarel : latin:/?Symmetry =
include ?Relation/metarel❙
theory Transitivity =
include ?Relation❙
structure metarel : latin:/?Transitivity =
include ?Relation/metarel❙
theory Preorder =
include ?Reflexivity❙
include ?Transitivity❙
theory EquivalenceRelation =
include ?Preorder❙
include ?Symmetry❙
theory AntiSymmetry =
include ?Relation❙
antisym : {x,y} ⊦ x$y ⟶ ⊦ y$x ⟶ ⊦ x≐y❙
theory Order =
include ?Preorder❙
include ?AntiSymmetry❙
......@@ -19,12 +19,8 @@ theory BiMagma =
theory Ringoid =
include ?BiMagma ❙
structure add : ?Commutative =
include ?BiMagma/add ❙
left_distrib: ⊦ ∀[r]∀[x]∀[y] r ⋅ (x + y) ≐ r⋅x + r ⋅ y ❙
right_distrib: ⊦ ∀[r]∀[x]∀[y] (x + y) ⋅ r ≐ x ⋅ r + y ⋅ r ❙
left_distrib: ⊦ ∀[r]∀[x]∀[y] r⋅(x+y) ≐ r⋅x + r⋅y ❙
right_distrib: ⊦ ∀[r]∀[x]∀[y] (x+y)⋅r ≐ x⋅r + y⋅r ❙
theory CommRingoid =
......@@ -34,69 +30,92 @@ theory CommRingoid =
theory MonoidalRingoid =
include ?Ringoid❙
structure add : ?Monoid =
include ?BiMagma?add❙
elem # zero❙
theory BiMonoid =
include ?MonoidalRingoid❙
structure mult : ?Monoid =
include ?BiMagma?mult❙
elem # one❙
theory NonZeroInvertible =
include ?BiMonoid❙
multinverse : ⊦ ∀[x] ¬x≐zero ⇒ ∃[y] mult/inverse x y❙
theory NoZeroDividers =
include ?BiMonoid ❙
no_zero_div: ⊦ ∀[x]∀[y] (x⋅y ≐ zero) ⇒ ((x ≐ zero) ∨ (y ≐ zero)) ❙
theory NonTrivial =
include ?BiMonoid❙
neq01: ⊦ ¬(zero ≐ one)❙
theory Semiring =
include ?Ringoid
include ?BiMonoid
structure add : ?CommMonoid =
include ?Ringoid/add ❙
elem # zero ❙
structure mult : ?Monoid =
include ?BiMagma/mult ❙
elem # one ❙
include ?MonoidalRingoid/add ❙
theory CommSemiring =
include ?CommRingoid ❙
include ?Semiring ❙
include ?CommRingoid ❙
theory NearRing =
include ?Semiring
include ?BiMonoid
structure add : ?Group =
include ?BiMagma/add ❙
include ?MonoidalRingoid/add ❙
inv # - 1 prec 45❙
div # 1 - 2 prec 40❙
theory CommNearRing =
include ?CommRingoid ❙
include ?NearRing ❙
include ?CommRingoid ❙
theory Ring =
include ?Semiring ❙
include ?NearRing❙
// realize ?Semiring❙
structure add : ?CommGroup =
include ?BiMagma/add ❙
include ?NearRing/add ❙
theory BooleanRing =
include ?Ring ❙
structure mult : ?IdempotentMonoid =
include ?Semiring/mult
include ?BiMonoid/mult
theory CommRing =
include ?CommRingoid ❙
include ?Ring ❙
include ?CommRingoid ❙
theory IntegralDomain =
include ?CommRing ❙
no_zero_div: ⊦ ∀[x]∀[y] (x⋅y ≐ zero) ⇒ ((x ≐ zero) ∨ (y ≐ zero))
include ?NoZeroDividers
theory SkewField =
include ?Ring ❙
structure mult : ?Group =
include ?Semiring/mult ❙
neq01: ⊦ ¬(zero ≐ one) ❙
theory DivisionRing =
include ?SkewField ❙
include ?NonZeroInvertible❙
include ?NonTrivial❙
theory Field =
......@@ -107,17 +126,16 @@ theory Field =
theory BilinearRingoid =
include ?Ringoid ❙
f: U ⟶ U ⟶ U ❙
bilinear: ⊦ ∀[x]∀[y]∀[z] (f (x + y) z) ≐ (f x z) + (f y z) ∧ (f x (y + z)) ≐ (f x y) + (f y z) ❙
bilinear: ⊦ ∀[x]∀[y]∀[z] (f (x+y) z) ≐ (f x z) + (f y z) ∧ (f x (y+z)) ≐ (f x y) + (f y z) ❙
homogen: ⊦ ∀[r]∀[x]∀[y] f (r⋅x) y ≐ r⋅ (f x y) ∧ f x (r⋅y) ≐ r⋅(f x y) ❙
theory LieRing =
theory LieRing =
include ?Ring❙
include ?BilinearRingoid ❙
structure A : ?CommGroup =
include ?Ringoid/add ❙
bracket = f ❘# ⟨ 1 2 ⟩ prec 40 ❙
bracket_defn: ⊦ ∀[x]∀[y] ⟨x y⟩ ≐ x ⋅ y - y ⋅ x ❙
jacobi: ⊦ ∀[x]∀[y]∀[z] ⟨x ⟨y z⟩⟩ + ⟨y ⟨z x⟩⟩ + ⟨z ⟨x y⟩⟩ ≐ O
alternating: ⊦ ∀[x] ⟨x x⟩ ≐ O
bracket_defn: ⊦ ∀[x]∀[y] ⟨x y⟩ ≐ x⋅y - y⋅x ❙
jacobi: ⊦ ∀[x]∀[y]∀[z] ⟨x ⟨y z⟩⟩ + ⟨y ⟨z x⟩⟩ + ⟨z ⟨x y⟩⟩ ≐ zero
alternating: ⊦ ∀[x] ⟨x x⟩ ≐ zero
......@@ -33,8 +33,8 @@ theory HOL =
theory HOLND =
include ?HOL❙
include ?IHOLND❙
include ?SFOLND❙
include ?SimpleFunctionsEta❙
include ?Classical❙
eq_equiv: {F,G} ⊦F≐G ⟶ ⊦F⇔G❘= [F,G,p] equivI ([q] p congP ([u]u) q) ([q] (p sym) congP ([u]u) q)❙
equiv_eq: {F,G} ⊦F⇔G ⟶ ⊦F≐G❘= [F,G,p] propext ([q] p equivEl q) ([q] p equivEr q)❙
......
......@@ -48,9 +48,14 @@ theory Worlds : latin:/?HOLND =
{T} ((tm S ⟶ tm T) ⟶ (tm S ⟶ prop)) ⟶ (tm S ⟶ prop)❘
= [S][B][T][F][x] B (S→T) [f] F (apply1 f) x❘
# liftbind 2❙
ref latin:/?DisjunctionHilbert2ND❚
ref latin:/?NegationHilbert2ND❚
ref latin:/?ImplicationHilbert2ND❚
ref latin:/?EquivalenceHilbert2ND❚
theory KripkeFrame : latin:/?TypedLogic =
include ?Worlds❙
accessible : tm W ⟶ tm W ⟶ prop❘ # 1 acc 2 prec 30❙
......@@ -61,13 +66,17 @@ theory KripkeModel =
include ?KripkeFrame❙
view LogicSemantics : latin:/?Logic → ?Worlds =
view PropSemantics : latin:/?Propositions → ?Worlds =
prop = tm W ⟶ prop❙
view LogicSemantics : latin:/?Logic → ?Worlds =
include ?PropSemantics❙
ded = [f] {w} ⊦ f w❙
view PLSemantics : latin:/?PL → ?Worlds =
include ?LogicSemantics❙
include ?PropSemantics❙
true = lift0 true❙
false = lift0 false❙
and = lift2 and❙
......@@ -79,6 +88,7 @@ view PLSemantics : latin:/?PL → ?Worlds =
view PLHilbertSemantics : latin:/?PLHilbert → ?Worlds =
include ?PLSemantics❙
include ?LogicSemantics❙
trueI = [w] trueI❙
falseE = [f] [g,w] f w falseE inconE❙
......@@ -89,11 +99,16 @@ view PLHilbertSemantics : latin:/?PLHilbert → ?Worlds =
orIl = [F,G,f] [w] f w orIl❙
orIr = [F,G,f] [w] f w orIr❙
orE_ax = [F,G,H][w] orE_ax❙
impE = [F,G,fg,f] [w] (fg w) impE (f w)❙
K_ax = [F,G,w] K_ax❙
S_ax = [F,G,H,w] S_ax❙
notI_ax = [F,w] notI_ax❙
notE = [F,nf,f] [g,w] (nf w) notE (f w) inconE❙
equivI_ax = [F,G,w] equivI_ax❙
equivEl = [F,G,fg,f] [w] (fg w) equivEl (f w)❙
equivEr = [F,G,fg,g] [w] (fg w) equivEr (g w)❙
......@@ -109,6 +124,7 @@ view TermSemantics : latin:/?TypedTerms → ?Worlds =
view SFOLSemantics : latin:/?SFOLEQ → ?Worlds =
include ?TermSemantics❙
include ?PLSemantics❙
include ?LogicSemantics❙
forall = liftbind forall❙
exists = liftbind exists❙
equal = [S] liftFun2 (equal S)❙
......@@ -116,6 +132,7 @@ view SFOLSemantics : latin:/?SFOLEQ → ?Worlds =
view MLSemantics : latin:/?ML → ?KripkeModel =
include ?PLSemantics❙
include ?LogicSemantics❙
box = [p] [v] ∀ [w] v acc w ⇒ p w❙
diamond = [p] [v] ∃ [w] v acc w ∧ p w❙
......
namespace latin:/❚
/T A fully modular specification of intuitionistic and classical propositional
logics. Every connective is specified in its own theory to maximize reusability.
Interdefinability of logics is formalized in various views.
logics.
Every connective and all proof rules are specified in their own theories to maximize reusability.
Proof rules follow natural deduction except that a judgment for inconsistency is used in some rules.
/T Naming conventions for theory name suffixes
* ND: natural deduction rules
* I resp. E: introduction resp. elimination rules
import rules scala://lf.mmt.kwarc.info❚
......@@ -172,6 +179,7 @@ theory IPL =
theory IPLND =
include ?IPL❙
include ?Logic❙
include ?TruthND❙
include ?FalsityND❙
include ?NegationND❙
......@@ -231,7 +239,7 @@ theory DependentConjunctionND =
/T Disjunction where the second disjunct's well-formedness may depend on the falsity of the first disjunct