Definition df-dc 843

Description: Propositions which are known to be true or false are called decidable. The (classical) Law of the Excluded Middle corresponds to the principle that all propositions are decidable, but even given intuitionistic logic, particular kinds of propositions may be decidable (for example, the proposition that two natural numbers are equal will be decidable under most sets of axioms).

Our notation for decidability is a connective DECID which we place before the formula in question. For example, DECID 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 is decidable".

We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 861, exmiddc 844, peircedc 922, or notnotrdc 851, any of which would correspond to the assertion that all propositions are decidable.

(Contributed by Jim Kingdon, 11-Mar-2018.)

Assertion

Ref	Expression
df-dc	⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

Detailed syntax breakdown of Definition df-dc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wdc 842	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 716	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  844  pm2.1dc  845  dcbid  846  dcim  849  dcn  850  notnotrdc  851  stdcndc  853  stdcndcOLD  854  stdcn  855  dcnnOLD  857  nndc  859  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.13dc  893  pm2.25dc  901  pm2.85dc  913  pm5.12dc  918  pm5.14dc  919  pm5.55dc  921  peircedc  922  pm5.54dc  926  dcand  941  dcor  944  pm5.62dc  954  pm5.63dc  955  pm4.83dc  960  ifpdc  988  xordc1  1438  biassdc  1440  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  19.30dc  1676  nfdc  1707  exmodc  2133  moexexdc  2167  dcne  2425  eueq2dc  2992  eueq3dc  2993  abvor0dc  3534  dcun  3621  ifcldcd  3662  ifnotdc  3663  ifandc  3665  ifmdc  3667  exmid01  4313  exmidsssnc  4318  exmidundif  4321  exmidundifim  4322  exmid1stab  4323  ontriexmidim  4646  ontri2orexmidim  4696  dcextest  4705  nndceq0  4742  nndceq  6734  nndcel  6735  fidceq  7126  fidcen  7158  tridc  7159  finexdc  7162  elssdc  7164  eqsndc  7165  unsnfidcex  7182  unsnfidcel  7183  undifdcss  7185  exmidssfi  7201  fissfi  7218  dcfi  7270  ctssdccl  7404  nninfisollem0  7423  nninfisollemne  7424  nninfisollemeq  7425  nninfisol  7426  fodjuomnilemdc  7437  omniwomnimkv  7460  exmidonfinlem  7498  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidaclem  7517  elni2  7631  indpi  7659  distrlem4prl  7901  distrlem4pru  7902  sup3exmid  9233  zdcle  9656  zdclt  9657  uzin  9890  elnn1uz2  9942  eluzdc  9945  xnn0dcle  10138  xrpnfdc  10178  xrmnfdc  10179  fztri3or  10376  fzdcel  10377  fzneuz  10439  exfzdc  10590  infssuzex  10597  qdclt  10609  fzfig  10796  fzowrddc  11343  sumdc  12047  zsumdc  12074  isum  12075  sum0  12078  fisumss  12082  isumss2  12083  fsumsplit  12097  sumsplitdc  12122  isumlessdc  12186  zproddc  12269  iprodap  12270  iprodap0  12272  prod0  12275  fprodssdc  12280  fprodsplitdc  12286  fprodsplit  12287  fprodunsn  12294  ef0lem  12350  nnwosdc  12739  prmdc  12831  pclemdc  12990  1arith  13069  ballotfilemcdc  13146  ennnfonelemdc  13167  ctiunctlemudc  13205  1loopgruspgr  16315  eupth2lem3lem4fi  16485  bj-trdc  16541  bj-fadc  16543  bj-dcstab  16545  bj-nndcALT  16547  decidi  16584  decidr  16585  bj-charfunr  16597  bddc  16615  subctctexmid  16791  triap  16830  dceqnconst  16863  dcapnconst  16864  nconstwlpolem0  16866  nconstwlpo  16869  dftest  16889