dftest - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > dftest		Unicode version

Theorem dftest 855

Description: A proposition is testable iff its negative or double-negative is true. See Chapter 2 [Moschovakis] p. 2.

Our notation for testability is DECID before the formula in question. For example, DECID corresponds to "x = y is testable". (Contributed by David A. Wheeler, 13-Aug-2018.)

**Assertion**
Ref	Expression
dftest	DECID $\/$

**Proof of Theorem dftest**
Step	Hyp	Ref	Expression
1		df-dc 776	1 DECID $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wb 103 $\/$ wo 661 DECID wdc 775

This theorem depends on definitions: df-dc 776

This theorem is referenced by: (None)

W3C validator