The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

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
-----------------------------