The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hello,

In most practical situations you are not in an empty environment,
and the latter contains arbitrarily complex formulas which,
together, might happen to be inconsistent.
Hence no cannot expect an answer such as
"current goal not provable", 
but at best "the current goal implies False".

This can be done for classical propositional logic for instance.

Hope this helps,
JF

On Tue, Jun 15, 2010 at 06:40:29PM +0200, Marko Maliković wrote:
> Dear mr. Auger,
> 
> Introduce a Hilbert-style propositional logic as a meta-theory.
> Frege-Lukas' Axioms and Modus Ponens as a inference rule we can introduce
> as follows:
> 
> Section Decidability.
> 
> Parameter imp : Prop -> Prop -> Prop.
> 
> Notation "s => t" := (imp s t) (at level 60, right associativity).
> 
> Parameter not : Prop -> Prop.
> 
> Axiom H1 : forall p q : Prop, p => q => p.
> Axiom H2 : forall p q r : Prop, (p => q => r) => (p => q) => p => r.
> Axiom H3 : forall p q : Prop, (not q => not p) => (p => q).
> 
> Axiom MP : forall p q : Prop, p -> p => q -> q.
> 
> Suppose we want to prove many statements but we do not know whether there
> are valid. One can be:
> 
> forall p q r : Prop, (p => q) => ((q => r) => (p => r)).
> 
> If we create some script which will try to prove such statements by
> automatism, then some statements will be proven but some will not be
> proven. For those that will not be proven, there are two cases:
> 
> 1. Statement is valid but our automatic script failed to prove
> 2. Statement is not provable (not valid)
> 
> In case number 2, I want that Coq "say" me that they are not provable.
> I want "proof" that the statement is not provable!!!
> 
> Thank you very much,
> 
> Marko Maliković
> 
> > Le Tue, 15 Jun 2010 14:39:58 +0200, Marko Maliković 
> > <marko AT ffri.hr>
> >  a
> > ĂŠcrit:
> >
> >> Dear Coq contributors and users,
> >>
> >> My question is: What is the situation in Coq with a decidability in the
> >> sense that if a formula is not derivable (provable) from a set of
> >> hypotheses, Coq can conclude that formula is not decidable. To be clear,
> >> I
> >> do not speak about the methods which can be modeled in Coq (like i.e.
> >> Davis–Putnam procedure). I am interested in whether and for what areas
> >> there exists automatisms in Coq which will tell you that something is
> >> decidable / not decidable.
> >
> > I wasn't aware of automatism in Coq telling that something is not
> > decidable...
> >
> > Have you example of such a thing?
> >
> > For decidability, I only know of "decide equality"; is this of this kind
> > of things you are talking?
> >
> >>
> >> Thank you very much,
> >>
> >> -----------------------
> >> Dr. Sc. Marko Maliković
> >> Filozofski fakultet
> >> Sveučilište u Rijeci
> >> ---------------------
> >> Ph.D. Marko Maliković
> >> Faculty of Arts and Sciences
> >> University of Rijeka, Croatia
> >> -----------------------------
> >>
> >
> >
> > --
> > CĂŠdric AUGER
> >
> > Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
> >
> 
> 
> -----------------------
> Dr. Sc. Marko Maliković
> Filozofski fakultet
> Sveučilište u Rijeci
> ---------------------
> Ph.D. Marko Maliković
> Faculty of Arts and Sciences
> University of Rijeka, Croatia
> -----------------------------
> 
> 
> 

-- 
Jean-Francois Monin
CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458