Propositions

Prop is the type of propositions. A proposition is a statement that could be true or false. Prop is very similar to Bool; the main difference is that whereas any Bool can always be evaluated to see if it is T or F, this may not be possible for a Prop due to the use of quantifiers (forall and exists).

Any Boolean expression can be used as a proposition. For example, T, x > 5, and (x < y) -> ((x == 2) \/ (x == 3)) can all be used as propositions.

However, unlike Boolean expressions, propositions can use quantifiers, that is, forall or exists. For example, forall x : Z. x^2 >= 0 is a Prop (but not a Bool).

If you type a proposition at the Disco prompt, it will simply print <Prop> and refuse to evaluate it. If you want to get an idea of whether a proposition is true or false, you have two options:

• The built-in holds function tries its best to determine whether a proposition is true or false. If it returns a value at all, it is definitely correct. For example,

  • holds ((5 < 3) \/ ((2 < 1) -> F)) yields T

  • holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p)) yields T

  • holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q)) yields F

  • holds (forall n:N. n < 529) yields F

  However, sometimes it may simply get stuck in an infinite loop. For example, holds (forall n:N. n >= 0) will simply get stuck. Even though it is obvious to us that this proposition is true, holds is not smart enough to see this; it simply tries evaluating n >= 0 for every natural number, which will never finish.

• One can also use the :test command. This command makes a best effort to evaluate a proposition, but only trying a finite number of examples for infinite domains. Additionally, in many cases it can output much more information than a simple T or F, for example, showing a counterexample if a forall is false, or a witness if an exists is true. For example,

  • :test forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q) prints

    - Certainly false: ∀p. ∀q. p \/ q <-> p /\ q
      Counterexample:
        p = F
        q = T
    

  • However, :test forall n:N. n < 529 prints

    - Possibly true: ∀n. n < 529
      Checked 100 possibilities without finding a counterexample.
    

    Obviously this proposition is false, but Disco apparently does not try a big enough value of n to be able to tell.

Note that at the moment it is not possible to combine propositions using logical operators like /\, \/, or ->. For example, Disco does not currently accept something like (forall x : N. x >= 0) /\ (exists x : N. x == 3), although this is certainly a proposition from a mathematical point of view. This is something that may be added in the future.