Кіріспе
Математикалық логикада Фрегедің пропозициялық калькулы пропозициялық калькулдың алғашқы аксиомалық жүйесі болды. Оны 1879 жылы Готтлоб Фреге ойлап тапты, ол предикаттық калькулдың да авторы, екінші реттік предикаттық калькулының бір бөлігі ретінде (бірақ «екінші реттік» терминін алғаш рет Чарльз Пирс қолданған және Фрегеден тәуелсіз предикаттық калькулының өзінің нұсқасын жасаған). Ол тек екі логикалық операторды қолданады: импликация және жоққа шығару, және ол алты аксиома мен бір қорытынды ережесінен тұрады: modus ponens. Аксиомалар Қорытындылау ережесі THEN 1 A → (B → A) THEN 2 (A → (B → C)) → ((A → B) → (A → C)) THEN 3 (A → (B → C)) → (B → (A → C)) FRG 1 (A → B) → (¬B → ¬A) FRG 2 ¬¬A → A FRG 3 A → ¬¬AMP P, P→Q ⊢ Q Фрегедің пропозициялық калькулы кез келген басқа классикалық пропозициялық калькулмен, мысалы, 11 аксиомасы бар «стандартты ПК» сияқты, эквивалентті. Фрегенің ПК және стандартты ПК екі ортақ аксиоманы бөліседі: THEN 1 және THEN 2. THEN 1-ден THEN 3-ке дейінгі аксиомалар тек импликация операторын ғана қолданады (және анықтайды), ал FRG 1-ден FRG 3-ке дейінгі аксиомалар жоққа шығару операторын анықтайды. Келесі теоремалар Фреге ПК-ның «теорема кеңістігі» ішінде стандартты ПК-ның қалған тоғыз аксиомасын табуға бағытталған, бұл стандартты ПК теориясы Фреге ПК теориясының ішінде қамтылғандығын көрсетеді. (Теория, сондай-ақ, мысал ретінде, «теорема кеңістігі» деп аталады, бұл жақсы құрылған формулалардың әмбебап жиынының ішкі жиыны болып табылатын теоремалардың жиыны. Теоремалар қорытындылау ережелерімен бағытталған түрде байланыстырылған, дендриттік желі құрайды. Теорема кеңістігінің түбінде аксиомалар орналасқан, олар теорема кеңістігін генерациялайтын жиын топты тудырғандай «өсіреді».)
THEN 2 (A → (B → C)) → ((A → B) → (A → C))
THEN 3 (A → (B → C)) → (B → (A → C))
FRG 1 (A → B) → (¬B → ¬A)
FRG 2 ¬¬A → A
FRG 3 A → ¬¬AMP P, P→Q ⊢ Q
Frege's propositional calculus is equivalent to any other classical propositional calculus, such as the "standard PC" with 11 axioms. Frege's PC and standard PC share two common axioms: THEN 1 and THEN 2. Notice that axioms THEN 1 through THEN 3 only make use of (and define) the implication operator, whereas axioms FRG 1 through FRG 3 define the negation operator. The following theorems will aim to find the remaining nine axioms of standard PC within the "theorem space" of Frege's PC, showing that the theory of standard PC is contained within the theory of Frege's PC. (A theory, also called here, for figurative purposes, a "theorem space", is a set of theorems that are a subset of a universal set of well formed formulas. The theorems are linked to each other in a directed manner by inference rules, forming a sort of dendritic network. At the roots of the theorem space are found the axioms, which "generate" the theorem space much like a generating set generates a group.)
Ережелер
#wffreason1. Алғышарт1. А→(Б→А) СОНЫМЕН 13. Б→А МП 1,2. #wffreason1. Алғышарт1. А→(Б→С) негіз2. (А → (Б → С)) → ((А → Б) → (А → С)) ОСЫДАН 23. (А→Б)→(А→С) МП 1,2. #wffreason1. Алғышарт1. А→(Б→С) негіз2. (А → (Б → С)) → (Б → (А → С)) СОНЫМЕН 33. Б→(А→С) МП 1,2. #wffreason1. (А→Б)→(¬Б→¬А) FRG 12. А→Б жорамал3. ¬Б→¬А МП 2,1. #wffreason1. Б→С алғышарт2. (Б→С)→(А→(Б→С)) СОНЫМЕН 13. А→(Б→С) МП 1,24. (А→(Б→С))→((А→Б)→(А→С)) ОСЫДАН 25. (А→Б)→(А→С) МП 3,46. А→Б жорамал7. А→С МП 6,5.