# @@cite BSL.ps Artemov
# based on
#html S. Artemov, Explicit provability and constructive semantics, Bulletin of Symbolic Logic, volume 7, No.1, pp. 1-36, 2001
#
#html see also: discovery notes 23 Sep 2003
# <- http://www.w3.org/XML/9711theory/LogicOfProofs.lsl
# <- http://esw.w3.org/topic/LogicalReflection
@keywords is, of, a.
@prefix owl: .
@prefix s: .
@prefix log: .
@prefix : .
@prefix lp: .
@forAll s, t, st, ts, tc, F, G, FG, MAP.
proves s:domain Proof.
comp a owl:FunctionalProperty;
s:domain (Proof Proof).crossProduct;
s:range Proof.
check a owl:FunctionalProperty;
s:domain Proof; s:range Proof.
sum a owl:FunctionalProperty;
s:domain (Proof Proof).crossProduct;
s:range Proof.
# reflection
{ t proves F } => F.
# application
{ (t s) comp ts.
t proves { F => G }.
s proves F
}
=> { ts proves G }.
# GMP application
{ s proves F.
(MAP F) log:subst G.
(s MAP) genl t
}
=> { t proves G }.
# and-introduction
# @@generalize to N formulas
{ s proves F.
t proves G.
(F G) log:conjunction FG.
(s t) sum st.
} => { st proves FG }.
# RDF simple entailment
# (subsumes and-elimination)
{ s proves F.
(s G) specl t.
F log:includes G.
} => { t proves G }.
# proof checker
# { t proves F } => { t.check proves { t proves F } }.
{ t check tc.
t proves F. } => { tc proves { t proves F } }.
# sum
# { s proves F } => { (s t).sum proves F }.
{ (s t) sum st.
s proves F } => { st proves F }.
# { t proves F } => { (s t).sum proves F }.
{ (s t) sum st.
t proves F } => { st proves F }.
@forAll c, A.
#hmm... this is probably circular, using => for
# both the propositional implications symbol
# and the inference rule turnstile.
{ c a Proof.
A.quote a Axiom } => { c proves A }.
######
{ ?S [ s:domain ?C] ?O } => { ?S a ?C }.
{ ?S [ s:range ?C] ?O } => { ?O a ?C }.
######
@prefix lpex: .
@prefix : .
a1 lp:proves { Socrates a Man }.
a2 lp:proves { { Socrates a Man } => { Socrates a Mortal } }.
(a2 a1).lp:comp a lp:Proof. # i.e. it exists
a3 lp:proves { @forAll WHO. { WHO a Man } => { WHO a Mortal } }.
( (WHO Socrates)
{ @forAll WHO. { WHO a Man } => { WHO a Mortal } }
) log:subst { { Socrates a Man } => { Socrates a Mortal } }.
(a3 (WHO Socrates)).lp:genl a lp:Proof.
a4 lp:proves { sky color blue }.
(a1 a4).lp:sum a lp:Proof.
a5 lp:proves { sky color blue. air temp hot }.
(a5 {air temp hot}).lp:specl a lp:Proof.