- From: Jos De_Roo <jos.deroo@agfa.com>
- Date: Thu, 25 Sep 2003 23:41:23 +0200
- To: "Dan Connolly <connolly" <connolly@w3.org>
- Cc: Pat Hayes <phayes@ai.uwf.edu>, www-rdf-logic@w3.org
DanC:
> On Wed, 2003-09-24 at 18:41, Jos De_Roo wrote:
> [...]
> > Also triggered by your chump
> > http://rdfig.xmlhack.com/2003/09/23/2003-09-23.html#1064349895.329315
> > (which reminded me about what I read some years ago
> > http://www.cs.gc.cuny.edu/~sartemov/publications/spinoza.ps)
> <- http://www.cs.gc.cuny.edu/~sartemov/publ.html
>
> I'm studying this stuff, but I don't see how it deals
> with universal quantification. The basic inference
> step that cwm uses is generalized modus ponens, e.g.
>
> { ?X a :Man } => { ?X a :Mortal }.
> :socrates a :Man.
> ===========>
> :socratese a :Mortal.
>
> What's the analog in Artemov's LP?
I'm studying it too...
Looking into http://www.cs.gc.cuny.edu/~sartemov/publications/BSL.ps
[[
Definition 5.1. The language of Logic of Proofs (LP) contains
[] the language of classical propositional logic which includes
propositional variables, truth constants T, B, and boolean
connectives
[] proof variables x0 ... xn ..., proof constants a0 ... an ...
[] function symbols: monadic !, binary . and +
[] operator symbol of the type "term:formula"
[...]
Definition 5.2. We define the system LP0 in the language of LP.
Axioms:
[A0] Finite set of axiom schemes of classical propositional logic
[A1] t:F -> F "reflection"
[A2] t:(F -> G) -> (s:F -> (t.s):G) "application"
[A3] t:F -> !t:(t:F) "proof checker"
[A4] s:F -> (s+t):F, t:F -> (s+t):F "sum"
Rule of inference:
[R1] F -> G, F |- G "modus ponens"
The system LP is LP0 plus the rule
[R2] A |- c:A, if A is an axiom A0-A4, and c a proof constant
"axiom necessitation"
]]
no need for quantifiers in a language of logic of proof;
they belong to the object language of predicate logic
and they are for instance explicitly mentioned in proof
term
-->term<--
{ { [ iw:Variable "?X" ] = :socrates.
[ iw:Variable "?X" ] a :Man } =>
{ :socrates a :Man } } =>
{ :socrates a :Mortal }.
which is a proof of
-->:formula<--
:socrates a :Mortal.
hmm...
> > I'm not understanding how consistency can be proved -
> > for inconsistency tests I can understand that the proof is a
> > construction like {triples} => {{triples} inconsistentWith theory}
> > where {} is more or less like box-ing but for consistency ???
>
> Exhibiting a model is one (constructive?) way to prove consistency.
I believe he showed that consistency is a special
case of reflection (i.e. provableT(false)->false)
which is not provable; it is not a case of
his explicit reflection (which is provable)
i.e. there is no specific proof of false.
--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Thursday, 25 September 2003 17:42:28 UTC