The finite truth values are precisely the decidable truth values.

finite.v

(** Prop is a complete lattice. We can ask which propositions are finite. *)

Definition directed (D : Prop -> Prop) :=
  (exists p , D p) /\ forall p q, D p -> D q -> exists r, D r /\ (p -> r) /\  (q -> r).

(** A proposition p is finite when it has the following property:
    for any directed D, if p ≤ sup D then there is q ∈ D such that p ≤ q. *)
Definition finite (p : Prop) :=
  forall D, directed D ->
    (p -> exists q, D q /\ q) -> exists q, D q /\ (p -> q).

(* The finite propositions are the decidable ones. *)
Lemma finite_iff_decidable (p : Prop) :
  finite p <-> p \/ ~ p.
Proof.
  split.
  - intro Fp.
    pose (D := (fun (q : Prop) => ~ q \/ (q /\ p))).
    assert (dirD : directed D).
    { split.
      - exists False ; now left.
      - intros r q Dr Dq.
         exists (r \/ q).
         split.
         + unfold D in *. tauto.
         + tauto.
    }
    assert (p_supD : p -> exists q, D q /\ q).
    { intro Hp.
      exists p.
      unfold D.
      tauto. }
    destruct (Fp D dirD p_supD) as [q [Dq pq]].
    unfold D in Dq.
    tauto.
  - intros [|].
    + intros D dirD G.
      destruct (G H) as [q [Dq qq]].
      now exists q.
    + intros D dirD G.
      destruct dirD as [[q Dq] _].
      now exists q.
Qed.