{"id":9280,"date":"2025-10-17T20:23:21","date_gmt":"2025-10-17T11:23:21","guid":{"rendered":"https:\/\/sasamath.com\/blog\/?page_id=9280"},"modified":"2026-09-27T12:32:49","modified_gmt":"2026-09-27T03:32:49","slug":"ch16-inference-rule-first-order-logic","status":"publish","type":"page","link":"https:\/\/sasamath.com\/blog\/invitation-to-mathematical-logic\/ch16-inference-rule-first-order-logic\/","title":{"rendered":"\uc77c\uacc4\ub17c\ub9ac\uc758 \ucd94\ub860\uaddc\uce59"},"content":{"rendered":"<div class=\"mathlogic2025\"><!-- ################## --><\/p>\n<p><!-- \n\n<h2>16. \uc77c\uacc4\ub17c\ub9ac\uc758 \ucd94\ub860\uaddc\uce59<\/h2>\n\n --><\/p>\n<p>\uc774\uc81c \uc758\ubbf8\ub860\uacfc \ube44\uad50\ud560 \uc77c\uacc4\ub17c\ub9ac\uc758 \ud615\uc2dd\ucd94\ub860\uacc4\ub97c \uc815\ud55c\ub2e4. \uc774 \uc7a5\uc5d0\uc11c\ub294 \uac00\uc815\uc73c\ub85c \uc0ac\uc6a9\ud558\ub294 \ub17c\ub9ac\uc2dd\ub4e4\uc744 \ubb38\uc7a5\uc73c\ub85c \uc81c\ud55c\ud55c\ub2e4. \ub530\ub77c\uc11c \uc804\uce6d \uc77c\ubc18\ud654 \uaddc\uce59\uc744 \uc0ac\uc6a9\ud560 \ub54c \uc790\uc720\ubcc0\uc218\ub97c \uac00\uc9c4 \uac00\uc815 \ub54c\ubb38\uc5d0 \uc0dd\uae30\ub294 \ubd80\uac00\uc870\uac74\uc744 \ub530\ub85c \uc801\uc744 \ud544\uc694\uac00 \uc5c6\ub2e4. \uc790\uc720\ubcc0\uc218\ub97c \uac00\uc9c4 \uac00\uc815\uae4c\uc9c0 \ud5c8\uc6a9\ud558\ub824\uba74 \uc77c\ubc18\ud654\ub418\ub294 \ubcc0\uc218\uac00 \ubaa8\ub4e0 \ubbf8\ud574\uc81c \uac00\uc815\uc5d0\uc11c \uc790\uc720\ub86d\uac8c \ub098\ud0c0\ub098\uc9c0 \uc54a\ub294\ub2e4\ub294 \ud45c\uc900\uc801\uc778 \uc81c\ud55c\uc774 \ud544\uc694\ud558\ub2e4.<\/p>\n<p>\uba85\uc81c\ub17c\ub9ac\uc640 \ub9c8\ucc2c\uac00\uc9c0\ub85c \ub2e4\uc74c \uc138 \uacf5\ub9ac\ud2c0\uc744 \uc0ac\uc6a9\ud55c\ub2e4.<\/p>\n<ul>\n<li>(A1) \\(\\phi\\to(\\psi\\to\\phi)\\)<\/li>\n<li>(A2) \\((\\phi\\to(\\psi\\to\\theta))\\to((\\phi\\to\\psi)\\to(\\phi\\to\\theta))\\)<\/li>\n<li>(A3) \\((\\neg\\phi\\to\\neg\\psi)\\to(\\psi\\to\\phi)\\)<\/li>\n<\/ul>\n<p>\ud55c\uc815\uae30\ud638\ub97c \uc704\ud55c \uacf5\ub9ac\ud2c0\uc740 \ub2e4\uc74c\uacfc \uac19\ub2e4.<\/p>\n<ul>\n<li>(A4) \\((\\forall x)\\phi\\to\\phi[t\/x]\\), \ub2e8 \\(t\\)\ub294 \\(\\phi\\)\uc5d0\uc11c \\(x\\)\uc5d0 \ub300\ud574 \uc790\uc720\ub86d\uac8c \ub300\uc785 \uac00\ub2a5\ud558\ub2e4.<\/li>\n<li>(A5) \\((\\forall x)(\\phi\\to\\psi)\\to(\\phi\\to(\\forall x)\\psi)\\), \ub2e8 \\(x\\)\ub294 \\(\\phi\\)\uc5d0\uc11c \uc790\uc720\ub86d\uac8c \ub098\ud0c0\ub098\uc9c0 \uc54a\ub294\ub2e4.<\/li>\n<\/ul>\n<p>\ub4f1\ud638\ub97c \uc704\ud55c \uacf5\ub9ac\ud2c0\uc740 \ub2e4\uc74c\uacfc \uac19\ub2e4.<\/p>\n<ul>\n<li>(E1) \\(t=t\\)<\/li>\n<li>(E2) \\((t=u)\\to(u=t)\\)<\/li>\n<li>(E3) \\((t=u)\\to((u=v)\\to(t=v))\\)<\/li>\n<li>(E4) \\((t=u)\\to(\\phi[t\/x]\\to\\phi[u\/x])\\), \ub2e8 \\(t,u\\)\ub294 \ubaa8\ub450 \\(\\phi\\)\uc5d0\uc11c \\(x\\)\uc5d0 \ub300\ud574 \uc790\uc720\ub86d\uac8c \ub300\uc785 \uac00\ub2a5\ud558\ub2e4.<\/li>\n<\/ul>\n<p>(E4)\ub294 \uac19\uc740 \ub300\uc0c1\uc744 \ub17c\ub9ac\uc2dd \uc548\uc5d0\uc11c \uc11c\ub85c \ubc14\uafb8\uc5b4\ub3c4 \uc9c4\ub9bf\uac12\uc774 \ubcc0\ud558\uc9c0 \uc54a\ub294\ub2e4\ub294 \ub4f1\ud638\uc758 \uce58\ud658 \uc6d0\ub9ac\ub97c \ub098\ud0c0\ub0b8\ub2e4.<\/p>\n<p>\ucd94\ub860\uaddc\uce59\uc740 \ub2e4\uc74c \ub450 \uac00\uc9c0\uc774\ub2e4.<\/p>\n<ol class=\"parenthesis\">\n<li>(R1) <span class=\"defined\">MP<\/span>: \\(\\phi\\)\uc640 \\(\\phi\\to\\psi\\)\ub85c\ubd80\ud130 \\(\\psi\\)\ub97c \ucd94\ub860\ud55c\ub2e4.<\/li>\n<li>(R2) <span class=\"defined\">\uc804\uce6d \uc77c\ubc18\ud654<\/span>: \\(\\phi\\)\ub85c\ubd80\ud130 \\((\\forall x)\\phi\\)\ub97c \ucd94\ub860\ud55c\ub2e4.<\/li>\n<\/ol>\n<p>\ubb38\uc7a5\ub4e4\uc758 \uc9d1\ud569 \\(\\varSigma\\)\uc5d0\uc11c \ucd9c\ubc1c\ud558\uc5ec \uc704 \uacf5\ub9ac\ud2c0\uacfc \ucd94\ub860\uaddc\uce59\uc744 \uc0ac\uc6a9\ud558\uc5ec \ub17c\ub9ac\uc2dd \\(\\phi\\)\ub97c \uc99d\uba85\ud560 \uc218 \uc788\uc73c\uba74<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\phi<br \/>\n\\]<br \/>\n\ub77c\uace0 \uc4f4\ub2e4.<\/p>\n<div class=\"problem\">\n<p class=\"marginbottomhalf\"><span class=\"problem\">\ubb38\uc81c 16.1.<\/span><br \/>\n\uc0c1\uc218\uae30\ud638 \\(c\\), 1\ud56d \uad00\uacc4\uae30\ud638 \\(P\\), \\(Q\\), 2\ud56d \uad00\uacc4\uae30\ud638 \\(R\\)\uc774 \uc788\ub2e4\uace0 \ud558\uc790. \ub2e4\uc74c \ub17c\ub9ac\uc2dd\uc774 (A4) \ub610\ub294 (A5)\ub85c\ubd80\ud130 \uace7\ubc14\ub85c \uc5bb\uc744 \uc218 \uc788\ub294 \uc2dd\uc778\uc9c0 \ud310\uc815\ud558\uc2dc\uc624. \uc62c\ubc14\ub974\uc9c0 \uc54a\uc73c\uba74 \uc5b4\ub290 \ubd80\uac00\uc870\uac74\uc774 \uc2e4\ud328\ud558\ub294\uc9c0 \uc124\uba85\ud558\uc2dc\uc624.<\/p>\n<ol class=\"parenthesis\">\n<li>\\((\\forall x)P(x)\\to P(c)\\).<\/li>\n<li>\\((\\forall x)(\\exists y)R(x,y)\\to(\\exists y)R(y,y)\\).<\/li>\n<li>\\((\\forall x)(P(y)\\to Q(x))\\to(P(y)\\to(\\forall x)Q(x))\\).<\/li>\n<li>\\((\\forall x)(P(x)\\to Q(x))\\to(P(x)\\to(\\forall x)Q(x))\\).<\/li>\n<\/ol>\n<p>(2)\uc5d0\uc11c \ub2e8\uc21c\ud55c \uae30\ud638 \uce58\ud658\uc774 \ubcc0\uc218 \ud3ec\ud68d\uc744 \uc77c\uc73c\ud0a4\ub294 \uacfc\uc815\uc744 \uad6c\uccb4\uc801\uc73c\ub85c \uc124\uba85\ud558\uc2dc\uc624.<\/p>\n<\/div>\n<div class=\"box theorem\">\n<p><span class=\"definition\">\uc815\uc758 16.1. (\uc77c\uacc4\ub17c\ub9ac\uc758 \ubb34\ubaa8\uc21c\uc131)<\/span><\/p>\n<p>\ubb38\uc7a5\ub4e4\uc758 \uc9d1\ud569 \\(\\varSigma\\)\uc5d0 \ub300\ud574 \uc5b4\ub5a4 \ubb38\uc7a5 \\(\\phi\\)\ub3c4<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\phi<br \/>\n\\quad\\text{\uc640}\\quad<br \/>\n\\varSigma\\vdash\\neg\\phi<br \/>\n\\]<br \/>\n\ub97c \ub3d9\uc2dc\uc5d0 \ub9cc\uc871\uc2dc\ud0a4\uc9c0 \uc54a\uc73c\uba74 \\(\\varSigma\\)\uac00 <span class=\"defined\">\ubb34\ubaa8\uc21c<\/span>(consistent)\uc774\ub77c\uace0 \ud55c\ub2e4.<\/p>\n<\/div>\n<div class=\"problem\">\n<p><span class=\"problem\">\ubb38\uc81c 16.2.<\/span><br \/>\n\\[<br \/>\n\\varSigma=\\{(\\forall x)(P(x)\\to Q(x)),\\;(\\forall x)P(x)\\}<br \/>\n\\]<br \/>\n\ub77c\uace0 \ud558\uc790. (A4), MP, \uc804\uce6d \uc77c\ubc18\ud654\ub9cc\uc744 \uc0ac\uc6a9\ud558\uc5ec<br \/>\n\\[<br \/>\n\\varSigma\\vdash(\\forall x)Q(x)<br \/>\n\\]<br \/>\n\uc784\uc744 \ubcf4\uc774\uc2dc\uc624. \uc99d\uba85\uc758 \uac01 \uc904\uc5d0\uc11c \uc5b4\ub5a4 \uacf5\ub9ac\ud2c0 \ub610\ub294 \ucd94\ub860\uaddc\uce59\uc744 \uc0ac\uc6a9\ud588\ub294\uc9c0 \ud45c\uc2dc\ud558\uc2dc\uc624.<\/p>\n<\/div>\n<div class=\"problem\">\n<p class=\"marginbottomhalf\"><span class=\"problem\">\ubb38\uc81c 16.3.<\/span><br \/>\n\\(a,b,c\\)\uac00 \uc0c1\uc218\uae30\ud638\uc774\uace0 \\(R\\)\uc774 2\ud56d \uad00\uacc4\uae30\ud638\ub77c\uace0 \ud558\uc790. \ub4f1\ud638 \uacf5\ub9ac\ud2c0\uc744 \uc0ac\uc6a9\ud558\uc5ec \ub2e4\uc74c\uc744 \ud615\uc2dd\uc801\uc73c\ub85c \uc720\ub3c4\ud558\uc2dc\uc624.<\/p>\n<ol class=\"parenthesis\">\n<li>\\(a=b\\vdash b=a\\).<\/li>\n<li>\\(a=b,\\;b=c\\vdash a=c\\).<\/li>\n<li>\\(a=b,\\;R(a,c)\\vdash R(b,c)\\).<\/li>\n<\/ol>\n<p>(3)\uc5d0\uc11c\ub294 (E4)\uc5d0 \uc0ac\uc6a9\ud560 \ub17c\ub9ac\uc2dd \\(\\phi(x)\\)\ub97c \uba85\uc2dc\ud558\uc2dc\uc624.<\/p>\n<\/div>\n<p>\ub2e4\uc74c \ucd94\ub860 \uc815\ub9ac\ub294 <a href=\"\/blog\/invitation-to-mathematical-logic\/ch12-propositional-logic\">\uba85\uc81c\ub17c\ub9ac\uc758 \ucd94\ub860 \uc815\ub9ac<\/a>\uc640 \uac19\uc740 \uc5ed\ud560\uc744 \ud55c\ub2e4.<\/p>\n<div class=\"box theorem\">\n<p><span class=\"definition\">\uc815\ub9ac 16.2. (\uc77c\uacc4\ub17c\ub9ac\uc758 \ucd94\ub860 \uc815\ub9ac)<\/span><\/p>\n<p>\\(\\varSigma\\)\uac00 \ubb38\uc7a5\ub4e4\uc758 \uc9d1\ud569\uc774\uace0 \\(\\sigma\\)\uac00 \ubb38\uc7a5\uc774\uba74<br \/>\n\\[<br \/>\n\\varSigma\\cup\\{\\sigma\\}\\vdash\\phi<br \/>\n\\quad\\Longrightarrow\\quad<br \/>\n\\varSigma\\vdash\\sigma\\to\\phi.<br \/>\n\\]<\/p>\n<\/div>\n<div class=\"proof\">\n<p class=\"proofbegin\"><span class=\"proof\">\uc99d\uba85<\/span><br \/>\n\uc99d\uba85 \uae38\uc774\uc5d0 \ub300\ud55c \uc218\ud559\uc801 \uadc0\ub0a9\ubc95\uc744 \uc0ac\uc6a9\ud55c\ub2e4. \uacf5\ub9ac, \\(\\varSigma\\)\uc758 \uc6d0\uc18c, \uac00\uc815 \\(\\sigma\\), MP \ub2e8\uacc4\ub294 \uba85\uc81c\ub17c\ub9ac\uc758 \ucd94\ub860 \uc815\ub9ac\uc640 \uac19\ub2e4. \ub0a8\uc740 \uac83\uc740 \uc804\uce6d \uc77c\ubc18\ud654 \ub2e8\uacc4\uc774\ub2e4. \\(\\phi=(\\forall x)\\psi\\)\uac00 \\(\\psi\\)\uc5d0\uc11c \uc77c\ubc18\ud654\ub418\uc5b4 \uc5bb\uc5b4\uc84c\ub2e4\uace0 \ud558\uc790. \uadc0\ub0a9\uac00\uc815\uc5d0 \uc758\ud558\uc5ec<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\sigma\\to\\psi.<br \/>\n\\]<br \/>\n\uc804\uce6d \uc77c\ubc18\ud654\ub97c \uc801\uc6a9\ud558\uba74<br \/>\n\\[<br \/>\n\\varSigma\\vdash(\\forall x)(\\sigma\\to\\psi).<br \/>\n\\]<br \/>\n\\(\\sigma\\)\ub294 \ubb38\uc7a5\uc774\ubbc0\ub85c \\(x\\)\uac00 \\(\\sigma\\)\uc5d0\uc11c \uc790\uc720\ub86d\uac8c \ub098\ud0c0\ub098\uc9c0 \uc54a\ub294\ub2e4. \ub530\ub77c\uc11c (A5)\uc640 MP\ub97c \uc801\uc6a9\ud558\uc5ec<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\sigma\\to(\\forall x)\\psi<br \/>\n\\]<br \/>\n\ub97c \uc5bb\ub294\ub2e4.<span class=\"qed\"><\/span><\/p>\n<\/div>\n<div class=\"box theorem\">\n<p><span class=\"definition\">\uc815\ub9ac 16.3. (\uac74\uc804\uc131 \uc815\ub9ac)<\/span><\/p>\n<p>\\(\\varSigma\\)\uac00 \ubb38\uc7a5\ub4e4\uc758 \uc9d1\ud569\uc774\uace0 \\(\\phi\\)\uac00 \ubb38\uc7a5\uc77c \ub54c<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\phi<br \/>\n\\quad\\Longrightarrow\\quad<br \/>\n\\varSigma\\models\\phi.<br \/>\n\\]<br \/>\n\ud2b9\ud788 \\(\\vdash\\phi\\)\uc774\uba74 \\(\\models\\phi\\)\uc774\ub2e4.<\/p>\n<\/div>\n<div class=\"proof\">\n<p class=\"proofbegin\"><span class=\"proof\">\uc99d\uba85<\/span><br \/>\n\\(\\mathcal M\\models\\varSigma\\)\ub77c\uace0 \ud558\uace0, \uc99d\uba85 \uae38\uc774\uc5d0 \ub300\ud55c \uc218\ud559\uc801 \uadc0\ub0a9\ubc95\uc744 \uc0ac\uc6a9\ud558\uc5ec \uc99d\uba85\uc758 \uac01 \ub17c\ub9ac\uc2dd\uc774 \\(\\mathcal M\\)\uc5d0\uc11c \uc784\uc758\uc758 \ubcc0\uc218 \uac12\ub9e4\uae40 \uc544\ub798 \ucc38\uc784\uc744 \uc99d\uba85\ud55c\ub2e4. (A1)\u2013(A3)\uc740 \uba85\uc81c\ub17c\ub9ac\uc758 \ud56d\uc9c4\uc2dd\uc774\ub2e4. (A4)\ub294 \uce58\ud658\uc758 \uc758\ubbf8\uc640 \u201c\uc790\uc720\ub86d\uac8c \ub300\uc785 \uac00\ub2a5\u201d \uc870\uac74\uc73c\ub85c\ubd80\ud130 \ucc38\uc774\uace0, (A5)\ub294 \\(x\\)\uac00 \\(\\phi\\)\uc5d0\uc11c \uc790\uc720\ub86d\uc9c0 \uc54a\ub2e4\ub294 \uc870\uac74 \ub54c\ubb38\uc5d0 \ucc38\uc774\ub2e4. (E1)\u2013(E4)\ub294 \uc2e4\uc81c \ub3d9\uc77c\uc131\uc758 \uc131\uc9c8\uacfc <a href=\"\/blog\/invitation-to-mathematical-logic\/ch15-semantics-first-order-logic\">\ubcf4\uc870\uc815\ub9ac 15.4\uc758 \uce58\ud658 \ubcf4\uc870\uc815\ub9ac<\/a>\uc5d0 \uc758\ud558\uc5ec \uc720\ub3c4\ub41c\ub2e4. \\(\\varSigma\\)\uc758 \uc6d0\uc18c\ub294 \ubb38\uc7a5\uc774\ubbc0\ub85c \\(\\mathcal M\\models\\varSigma\\)\uc5d0 \uc758\ud574 \ubaa8\ub4e0 \uac12\ub9e4\uae40\uc5d0\uc11c \ucc38\uc774\ub2e4.<\/p>\n<p>MP\uac00 \ucc38\uc744 \ubcf4\uc874\ud558\ub294 \uac83\uc740 \ud568\uc758\uc758 \uc758\ubbf8\uc5d0\uc11c \ubc14\ub85c \uc720\ub3c4\ub41c\ub2e4. \uc804\uce6d \uc77c\ubc18\ud654\uc758 \uacbd\uc6b0 \uadc0\ub0a9\uac00\uc815\uc740 \\(\\phi\\)\uac00 \\(\\mathcal M\\)\uc5d0\uc11c \ubaa8\ub4e0 \uac12\ub9e4\uae40 \uc544\ub798 \ucc38\uc774\ub77c\ub294 \ub73b\uc774\ub2e4. \ub530\ub77c\uc11c \uc784\uc758\uc758 \uac12\ub9e4\uae40 \\(s\\)\uc640 \uc784\uc758\uc758 \\(a\\in M\\)\uc5d0 \ub300\ud574<br \/>\n\\[<br \/>\n\\mathcal M,s[x\\mapsto a]\\models\\phi<br \/>\n\\]<br \/>\n\uc774\uace0, \uace7<br \/>\n\\[<br \/>\n\\mathcal M,s\\models(\\forall x)\\phi<br \/>\n\\]<br \/>\n\uc774\ub2e4. \ub9c8\uc9c0\ub9c9 \ub17c\ub9ac\uc2dd \\(\\phi\\)\uac00 \ubb38\uc7a5\uc774\ubbc0\ub85c \\(\\mathcal M\\models\\phi\\)\ub97c \uc5bb\ub294\ub2e4.<span class=\"qed\"><\/span><\/p>\n<\/div>\n<div class=\"problem\">\n<p class=\"marginbottomhalf\"><span class=\"problem\">\ubb38\uc81c 16.4.<\/span><br \/>\n\uac74\uc804\uc131 \uc815\ub9ac\ub97c \uc0ac\uc6a9\ud558\uc5ec \ub2e4\uc74c\uc744 \ubcf4\uc774\uc2dc\uc624.<\/p>\n<ol class=\"parenthesis\">\n<li>\\(\\nvdash(\\exists x)P(x)\\to(\\forall x)P(x)\\).<\/li>\n<li>\\(\\{(\\forall x)P(x)\\}\\nvdash(\\exists x)\\neg P(x)\\).<\/li>\n<\/ol>\n<p>\uac01 \uacbd\uc6b0\uc5d0 \ub450 \uc6d0\uc18c \uc774\ud558\uc758 \uc601\uc5ed\uc744 \uac16\ub294 \ubc18\ub840 \uad6c\uc870\ub97c \uc9c1\uc811 \uc81c\uc2dc\ud558\uc2dc\uc624.<\/p>\n<\/div>\n<p>\ub2e4\uc74c\uc73c\ub85c \uc77c\uacc4\ub17c\ub9ac\uc758 \uc644\uc804\uc131\uc744 \uc0b4\ud3b4\ubcf4\uc790. \uc644\uc804\uc131\uc758 \ud575\uc2ec\uc740 \ubc18\ub300 \ubc29\ud5a5, \uc989 \ubb34\ubaa8\uc21c\uc778 \ubb38\uc7a5 \uc9d1\ud569\uc5d0\uc11c \uc2e4\uc81c \ubaa8\ud615\uc744 \ub9cc\ub4dc\ub294 \uc77c\uc774\ub2e4. \uba3c\uc800 \uc0c8 \uc0c1\uc218\ub97c \ub3c4\uc785\ud558\ub294 \ub2e8\uacc4\uac00 \ubb34\ubaa8\uc21c\uc131\uc744 \ubcf4\uc874\ud568\uc744 \ud655\uc778\ud55c\ub2e4.<\/p>\n<div class=\"box theorem\">\n<p><span class=\"definition\">\ubcf4\uc870\uc815\ub9ac 16.4. (\uc0c8 \uc0c1\uc218 \ubcf4\uc870\uc815\ub9ac)<\/span><\/p>\n<p>\\(\\varSigma\\)\uac00 \ubb34\ubaa8\uc21c\uc778 \ubb38\uc7a5 \uc9d1\ud569\uc774\uace0 \\((\\exists x)\\phi(x)\\)\uac00 \ubb38\uc7a5\uc774\uba70 \\(c\\)\uac00 \\(\\varSigma\\)\uc640 \\((\\exists x)\\phi(x)\\)\uc5d0 \ub098\ud0c0\ub098\uc9c0 \uc54a\ub294 \uc0c8 \uc0c1\uc218\uae30\ud638\ub77c\uace0 \ud558\uc790. \uadf8\ub7ec\uba74<br \/>\n\\[<br \/>\n\\varSigma\\cup\\{(\\exists x)\\phi(x)\\to\\phi(c)\\}<br \/>\n\\]<br \/>\n\ub3c4 \ubb34\ubaa8\uc21c\uc774\ub2e4.<\/p>\n<\/div>\n<div class=\"proof\">\n<p class=\"proofbegin\"><span class=\"proof\">\uc99d\uba85<\/span><br \/>\n\\(H=(\\exists x)\\phi(x)\\to\\phi(c)\\)\ub77c\uace0 \ud558\uc790. \\(\\varSigma\\cup\\{H\\}\\)\uac00 \ubaa8\uc21c\uc801\uc774\ub77c\uace0 \uac00\uc815\ud558\uba74 \ucd94\ub860 \uc815\ub9ac\uc640 \uba85\uc81c\ub17c\ub9ac\uc758 \ubc95\uce59\uc744 \uc0ac\uc6a9\ud558\uc5ec<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\neg H<br \/>\n\\]<br \/>\n\ub97c \uc5bb\ub294\ub2e4. \ub530\ub77c\uc11c<br \/>\n\\[<br \/>\n\\varSigma\\vdash(\\exists x)\\phi(x),<br \/>\n\\qquad<br \/>\n\\varSigma\\vdash\\neg\\phi(c)<br \/>\n\\]<br \/>\n\uac00 \ubaa8\ub450 \uc131\ub9bd\ud55c\ub2e4. \ub450 \ubc88\uc9f8 \uc99d\uba85\uc5d0\uc11c \uc0c8 \uc0c1\uc218 \\(c\\)\ub97c \uadf8 \uc99d\uba85\uc5d0 \uc4f0\uc774\uc9c0 \uc54a\uc740 \ubcc0\uc218 \\(y\\)\ub85c \uc77c\ub960\uc801\uc73c\ub85c \ubc14\uafb8\uba74, \\(c\\)\uac00 \\(\\varSigma\\)\uc5d0 \ub098\ud0c0\ub098\uc9c0 \uc54a\uc73c\ubbc0\ub85c<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\neg\\phi(y)<br \/>\n\\]<br \/>\n\uc778 \uc99d\uba85\uc744 \uc5bb\ub294\ub2e4. \uc804\uce6d \uc77c\ubc18\ud654\ub97c \uc801\uc6a9\ud558\uba74<br \/>\n\\[<br \/>\n\\varSigma\\vdash(\\forall y)\\neg\\phi(y),<br \/>\n\\]<br \/>\n\uc989 \ubcc0\uc218 \uc774\ub984\uc744 \ubc14\uafb8\uc5b4<br \/>\n\\[<br \/>\n\\varSigma\\vdash\\neg(\\exists x)\\phi(x)<br \/>\n\\]<br \/>\n\ub97c \uc5bb\ub294\ub2e4. \uc774\ub294 \\(\\varSigma\\)\uc758 \ubb34\ubaa8\uc21c\uc131\uc5d0 \ubaa8\uc21c\uc774\ub2e4.<span class=\"qed\"><\/span><\/p>\n<\/div>\n<div class=\"box theorem\">\n<p class=\"marginbottomhalf\"><span class=\"definition\">\ubcf4\uc870\uc815\ub9ac 16.5. (\ud5e8\ud0a8 \ud655\uc7a5)<\/span><\/p>\n<p>\\(\\mathcal L\\)\uc774 \uac00\uc0b0 \uc5b8\uc5b4\uc774\uace0 \\(\\varSigma\\)\uac00 \ubb34\ubaa8\uc21c\uc778 \\(\\mathcal L\\)-\ubb38\uc7a5 \uc9d1\ud569\uc774\uba74, \uc0c8\ub85c\uc6b4 \uc0c1\uc218\uae30\ud638\ub4e4\uc744 \uac00\uc0b0 \uac1c \ucd94\uac00\ud55c \uc5b8\uc5b4 \\(\\mathcal L^*\\)\uc640 \ub2e4\uc74c \uc131\uc9c8\uc744 \uac16\ub294 \uc644\uc804\ud55c \ubb34\ubaa8\uc21c \uc774\ub860 \\(T^*\\supseteq\\varSigma\\)\uac00 \uc874\uc7ac\ud55c\ub2e4.<\/p>\n<ol class=\"parenthesis\">\n<li>\ubaa8\ub4e0 \\(\\mathcal L^*\\)-\ubb38\uc7a5 \\(\\phi\\)\uc5d0 \ub300\ud574 \uc815\ud655\ud788 \ud558\ub098\uc758 \\(\\phi,\\neg\\phi\\)\uac00 \\(T^*\\)\uc5d0 \uc18d\ud55c\ub2e4.<\/li>\n<li>\\((\\exists x)\\phi(x)\\in T^*\\)\uc774\uba74 \uc5b4\ub5a4 \uc0c1\uc218\uae30\ud638 \\(c\\)\uac00 \uc874\uc7ac\ud558\uc5ec \\(\\phi(c)\\in T^*\\)\uc774\ub2e4.<\/li>\n<li>\\(T^*\\)\ub294 \uc5f0\uc5ed\uc801\uc73c\ub85c \ub2eb\ud600 \uc788\ub2e4. \uc989 \\(T^*\\vdash\\phi\\)\uc774\uba74 \\(\\phi\\in T^*\\)\uc774\ub2e4.<\/li>\n<\/ol>\n<\/div>\n<div class=\"proof\">\n<p class=\"proofbegin\"><span class=\"proof\">\uc99d\uba85 \uac1c\uc694<\/span><br \/>\n\uba3c\uc800 \uc11c\ub85c \ub2e4\ub978 \uc0c8 \uc0c1\uc218\uae30\ud638\ub4e4\uc758 \uac00\uc0b0 \uc9d1\ud569<br \/>\n\\[<br \/>\nC=\\{c_0,c_1,\\ldots\\}<br \/>\n\\]<br \/>\n\uc744 \uc900\ube44\ud558\uace0 \\(\\mathcal L^*=\\mathcal L\\cup C\\)\ub85c \ub454\ub2e4. \\(\\mathcal L^*\\)\ub3c4 \uac00\uc0b0\uc774\ubbc0\ub85c \uadf8 \ubb38\uc7a5\ub4e4\uacfc \uc874\uc7ac\ubb38\uc7a5\ub4e4\uc744 \ucc28\ub840\ub85c \ub098\uc5f4\ud560 \uc218 \uc788\ub2e4. \uc874\uc7ac\ubb38\uc7a5 \\((\\exists x)\\phi(x)\\)\ub97c \ub9cc\ub0a0 \ub54c\ub9c8\ub2e4 \uadf8 \ubb38\uc7a5\uacfc \ud604\uc7ac\uae4c\uc9c0\uc758 \uad6c\uc131\uc5d0 \ub098\ud0c0\ub098\uc9c0 \uc54a\uc740 \uc0c1\uc218 \\(c\\in C\\)\ub97c \ud558\ub098 \uace8\ub77c<br \/>\n\\[<br \/>\n(\\exists x)\\phi(x)\\to\\phi(c)<br \/>\n\\]<br \/>\n\ub97c \ucd94\uac00\ud55c\ub2e4. \ubcf4\uc870\uc815\ub9ac 16.4\uc5d0 \uc758\ud574 \uc774\ub7ec\ud55c \ud5e8\ud0a8 \ubb38\uc7a5\uc744 \ucd94\uac00\ud574\ub3c4 \ubb34\ubaa8\uc21c\uc131\uc774 \ubcf4\uc874\ub41c\ub2e4. \uadf8 \ub4a4 \uac01 \ubb38\uc7a5 \\(\\theta\\)\uc5d0 \ub300\ud574 \\(\\theta\\) \ub610\ub294 \\(\\neg\\theta\\) \uac00\uc6b4\ub370 \ubb34\ubaa8\uc21c\uc131\uc744 \ubcf4\uc874\ud558\ub294 \ud558\ub098\ub97c \ucc28\ub840\ub85c \ucd94\uac00\ud55c\ub2e4. \uc720\ud55c\ud55c \uc99d\uba85\uc740 \uc5b4\ub5a4 \uc720\ud55c \ub2e8\uacc4\uc5d0 \uc774\ubbf8 \ud3ec\ud568\ub418\ubbc0\ub85c \uc804\uccb4 \ud569\uc9d1\ud569\ub3c4 \ubb34\ubaa8\uc21c\uc774\ub2e4. \ub9c8\uc9c0\ub9c9\uc73c\ub85c \uadf8 \uc5f0\uc5ed\uc801 \ud3d0\ud3ec\ub97c \ucde8\ud558\uba74 \uc6d0\ud558\ub294 \\(T^*\\)\ub97c \uc5bb\ub294\ub2e4.<span class=\"qed\"><\/span><\/p>\n<\/div>\n<div class=\"box theorem\">\n<p><span class=\"definition\">\ubcf4\uc870\uc815\ub9ac 16.6. (\ud56d \ubaa8\ud615)<\/span><\/p>\n<p>\ubcf4\uc870\uc815\ub9ac 16.5\uc758 \\(T^*\\)\ub294 \ubaa8\ud615\uc744 \uac00\uc9c4\ub2e4.<\/p>\n<\/div>\n<div class=\"proof\">\n<p class=\"proofbegin\"><span class=\"proof\">\uc99d\uba85<\/span><br \/>\n\ub2eb\ud78c\ud56d\ub4e4\uc758 \uc9d1\ud569\uc5d0\uc11c<br \/>\n\\[<br \/>\nt\\sim u<br \/>\n\\quad\\Longleftrightarrow\\quad<br \/>\nT^*\\vdash t=u<br \/>\n\\]<br \/>\n\ub85c \uc815\uc758\ud55c\ub2e4. \ud544\uc694\ud558\uba74 \uc0c8 \uc0c1\uc218 \ud558\ub098\ub97c \ub354\ud558\uc5ec <span class=\"defined\">\ub2eb\ud78c\ud56d<\/span>(closed term)\uc774 \uc801\uc5b4\ub3c4 \ud558\ub098 \uc874\uc7ac\ud558\uac8c \ud55c\ub2e4. (E1)\u2013(E3)\uc5d0 \uc758\ud574 \uc704 \uad00\uacc4\ub294 \ub3d9\uce58\uad00\uacc4\uc774\ub2e4. \\([t]\\)\ub97c \\(t\\)\uc758 \ub3d9\uce58\ub958\ub77c\uace0 \ud558\uace0, \uc774 \ub3d9\uce58\ub958\ub4e4\uc758 \uc9d1\ud569\uc744 \uc601\uc5ed\uc73c\ub85c \uc0bc\ub294\ub2e4.<\/p>\n<p>\ud568\uc218\uae30\ud638\uc640 \uad00\uacc4\uae30\ud638\ub97c<br \/>\n\\[<br \/>\n\\begin{gathered}<br \/>\nf^{\\mathcal M}([t_1],\\ldots,[t_n])<br \/>\n=[f(t_1,\\ldots,t_n)],\\\\[3pt]<br \/>\n([t_1],\\ldots,[t_n])\\in R^{\\mathcal M}<br \/>\n\\quad\\Longleftrightarrow\\quad<br \/>\nR(t_1,\\ldots,t_n)\\in T^*<br \/>\n\\end{gathered}<br \/>\n\\]<br \/>\n\ub85c \ud574\uc11d\ud558\uace0 \\(c^{\\mathcal M}=\\)\ub85c \ub454\ub2e4. (E4)\uc5d0 \uc758\ud574 \ub300\ud45c\uc6d0\uc744 \ubc14\uafb8\uc5b4\ub3c4 \uacb0\uacfc\uac00 \ubcc0\ud558\uc9c0 \uc54a\uc73c\ubbc0\ub85c \uc774 \uc815\uc758\ub4e4\uc740 \uc798 \uc815\uc758\ub418\uc5b4 \uc788\ub2e4.<\/p>\n<p>\ub17c\ub9ac\uc2dd\uc758 \uad6c\uc870\uc5d0 \ub300\ud55c \uadc0\ub0a9\ubc95\uc744 \uc0ac\uc6a9\ud558\uc5ec \ub2e4\uc74c \uc9c4\ub9ac \ubcf4\uc870\uc815\ub9ac\ub97c \uc5bb\ub294\ub2e4. \\(\\phi\\)\uc758 \uc790\uc720\ubcc0\uc218\uac00 \\(x_1,\\ldots,x_n\\) \uac00\uc6b4\ub370\uc5d0 \uc788\uace0 \\(t_1,\\ldots,t_n\\)\uc774 \ub2eb\ud78c\ud56d\uc774\ub77c\uace0 \ud558\uc790. \\(s(x_i)=[t_i]\\)\uac00 \ub418\ub3c4\ub85d \uac12\ub9e4\uae40 \\(s\\)\ub97c \uc7a1\uc73c\uba74<br \/>\n\\[<br \/>\n\\mathcal M,s\\models\\phi<br \/>\n\\quad\\Longleftrightarrow\\quad<br \/>\n\\phi[t_1\/x_1,\\ldots,t_n\/x_n]\\in T^*.<br \/>\n\\]<br \/>\n\uc544\ud1b0\ub17c\ub9ac\uc2dd\uacfc \uacb0\ud569\uc790 \ub2e8\uacc4\ub294 \uc815\uc758\uc640 \\(T^*\\)\uc758 \uc644\uc804\uc131\uc5d0\uc11c \ub530\ub978\ub2e4.<\/p>\n<p>\uc804\uce6d \ud55c\uc815\uae30\ud638 \ub2e8\uacc4\uc5d0\uc11c \\((\\forall x)\\psi\\in T^*\\)\uc774\uba74 (A4)\uc5d0 \uc758\ud574 \ubaa8\ub4e0 \ub2eb\ud78c\ud56d \\(t\\)\uc5d0 \ub300\ud574 \\(\\psi[t\/x]\\in T^*\\)\uc774\ub2e4. \ubc18\ub300\ub85c \\((\\forall x)\\psi\\notin T^*\\)\uc774\uba74 \\(T^*\\)\uc758 \uc644\uc804\uc131\uc5d0 \uc758\ud558\uc5ec<br \/>\n\\[<br \/>\n\\neg(\\forall x)\\psi\\in T^*<br \/>\n\\]<br \/>\n\uc774\ub2e4. \uace0\uc804 \uba85\uc81c\ub17c\ub9ac\uc758 \uc774\uc911\ubd80\uc815 \ubc95\uce59\uacfc \ud55c\uc815\uae30\ud638 \uaddc\uce59\uc5d0 \uc758\ud558\uc5ec<br \/>\n\\[<br \/>\n\\neg(\\forall x)\\psi\\leftrightarrow(\\exists x)\\neg\\psi<br \/>\n\\]<br \/>\n\uac00 \uc99d\uba85 \uac00\ub2a5\ud558\ubbc0\ub85c<br \/>\n\\[<br \/>\n(\\exists x)\\neg\\psi\\in T^*<br \/>\n\\]<br \/>\n\uc774\ub2e4. \uc774\uc81c \ud5e8\ud0a8 \uc131\uc9c8\uc5d0 \uc758\ud558\uc5ec \uc801\ub2f9\ud55c \uc0c1\uc218 \\(c\\)\uc5d0 \ub300\ud558\uc5ec<br \/>\n\\[<br \/>\n\\neg\\psi\\in T^*<br \/>\n\\]<br \/>\n\uc774\ub2e4. \ub530\ub77c\uc11c \uc804\uce6d\ubb38\uc7a5\uc740 \ubaa8\ud615\uc5d0\uc11c\ub3c4 \uac70\uc9d3\uc774\ub2e4.<\/p>\n<p>\ud2b9\ud788 \ubaa8\ub4e0 \\(\\sigma\\in T^*\\)\uc5d0 \ub300\ud574 \\(\\mathcal M\\models\\sigma\\)\uc774\ub2e4. \ub530\ub77c\uc11c \\(\\mathcal M\\models T^*\\), \ub098\uc544\uac00 \\(\\mathcal M\\models\\varSigma\\)\uc774\ub2e4.<span class=\"qed\"><\/span><\/p>\n<\/div>\n<div class=\"problem\">\n<p class=\"marginbottomhalf\"><span class=\"problem\">\ubb38\uc81c 16.5.<\/span><br \/>\n\uc5b8\uc5b4 \\(\\mathcal L^*\\)\uc5d0 \uc0c1\uc218\uae30\ud638 \\(c,d\\), 1\ud56d \ud568\uc218\uae30\ud638 \\(f\\), 1\ud56d \uad00\uacc4\uae30\ud638 \\(P\\)\uac00 \uc788\ub2e4\uace0 \ud558\uc790. \uc644\uc804\ud55c \ud5e8\ud0a8 \uc774\ub860 \\(T^*\\)\uac00<br \/>\n\\[<br \/>\nT^*\\vdash c=d,<br \/>\n\\qquad<br \/>\nT^*\\vdash f(c)=d,<br \/>\n\\qquad<br \/>\nP(c)\\in T^*<br \/>\n\\]<br \/>\n\ub97c \ub9cc\uc871\uc2dc\ud0a8\ub2e4\uace0 \ud558\uc790. \ubcf4\uc870\uc815\ub9ac 16.6\uc758 \ud56d \ubaa8\ud615 \\(\\mathcal M\\)\uc5d0\uc11c \ub2e4\uc74c\uc744 \ubcf4\uc774\uc2dc\uc624.<\/p>\n<ol class=\"parenthesis\">\n<li>\\( [ c ] = [ d ] \\).<\/li>\n<li>\\(f^{\\mathcal M}( [ c ] ) = [ c ]\\).<\/li>\n<li>\\( [ c ] \\in P^{\\mathcal M}\\).<\/li>\n<li>\uc77c\ubc18\uc801\uc73c\ub85c \\( [ t ] = [ u ] \\)\uc774\uba74<br \/>\n\\[<br \/>\nP(t)\\in T^*<br \/>\n\\quad\\Longleftrightarrow\\quad<br \/>\nP(u)\\in T^*<br \/>\n\\]<br \/>\n\uc784\uc744 (E2), (E4), \\(T^*\\)\uc758 \uc5f0\uc5ed\uc801 \ub2eb\ud798\uc744 \uc0ac\uc6a9\ud558\uc5ec \uc124\uba85\ud558\uc2dc\uc624. \uc774\uac83\uc774 \uad00\uacc4\uae30\ud638\uc758 \ud574\uc11d\uc774 \ub300\ud45c\uc6d0\uc758 \uc120\ud0dd\uacfc \ubb34\uad00\ud568\uc744 \uc5b4\ub5bb\uac8c \ubcf4\uc7a5\ud558\ub294\uc9c0\ub3c4 \uc124\uba85\ud558\uc2dc\uc624.<\/li>\n<\/ol>\n<\/div>\n<div class=\"box theorem\">\n<p><span class=\"definition\">\uc815\ub9ac 16.7. (\uc644\uc804\uc131 \uc815\ub9ac)<\/span><\/p>\n<p>\\(\\mathcal L\\)\uc774 \uac00\uc0b0 \uc77c\uacc4\ub17c\ub9ac\uc5b8\uc5b4\uc774\uace0 \\(\\varSigma\\)\uac00 \\(\\mathcal L\\)-\ubb38\uc7a5\ub4e4\uc758 \uc9d1\ud569, \\(\\phi\\)\uac00 \\(\\mathcal L\\)-\ubb38\uc7a5\uc774\uba74<br \/>\n\\[<br \/>\n\\varSigma\\models\\phi<br \/>\n\\quad\\Longrightarrow\\quad<br \/>\n\\varSigma\\vdash\\phi.<br \/>\n\\]<br \/>\n\ub530\ub77c\uc11c<br \/>\n\\[<br \/>\n\\varSigma\\models\\phi<br \/>\n\\quad\\Longleftrightarrow\\quad<br \/>\n\\varSigma\\vdash\\phi.<br \/>\n\\]<\/p>\n<\/div>\n<div class=\"proof\">\n<p class=\"proofbegin\"><span class=\"proof\">\uc99d\uba85<\/span><br \/>\n\ub300\uc6b0\ub97c \ubcf4\uc778\ub2e4. \\(\\varSigma\\nvdash\\phi\\)\ub77c\uace0 \ud558\uc790. \ub9cc\uc57d<br \/>\n\\[<br \/>\n\\varSigma\\cup\\{\\neg\\phi\\}<br \/>\n\\]<br \/>\n\uac00 \ubaa8\uc21c\uc801\uc774\uba74 \ucd94\ub860 \uc815\ub9ac\uc640 \uace0\uc804 \uba85\uc81c\ub17c\ub9ac\uc758 \ubc95\uce59\uc744 \uc774\uc6a9\ud558\uc5ec \\(\\varSigma\\vdash\\phi\\)\ub97c \uc5bb\uc73c\ubbc0\ub85c \ubaa8\uc21c\uc774\ub2e4. \ub530\ub77c\uc11c \\(\\varSigma\\cup\\{\\neg\\phi\\}\\)\ub294 \ubb34\ubaa8\uc21c\uc774\ub2e4. \ubcf4\uc870\uc815\ub9ac 16.5\uc640 16.6\uc5d0 \uc758\ud574 \uc774\ub97c \ub9cc\uc871\uc2dc\ud0a4\ub294 \uad6c\uc870 \\(\\mathcal M\\)\uc774 \uc874\uc7ac\ud55c\ub2e4. \uadf8\ub7ec\uba74<br \/>\n\\[<br \/>\n\\mathcal M\\models\\varSigma,<br \/>\n\\qquad<br \/>\n\\mathcal M\\not\\models\\phi,<br \/>\n\\]<br \/>\n\uc774\ubbc0\ub85c \\(\\varSigma\\not\\models\\phi\\)\uc774\ub2e4.<span class=\"qed\"><\/span><\/p>\n<\/div>\n<p>\uac74\uc804\uc131\uacfc \uc644\uc804\uc131\uc744 \ud569\uce58\uba74 \uc77c\uacc4\ub17c\ub9ac\uc5d0\uc11c \uc758\ubbf8\ub860\uc801 \uadc0\uacb0\uacfc \ud615\uc2dd\uc801 \uc99d\uba85 \uac00\ub2a5\uc131\uc774 \uc815\ud655\ud788 \uc77c\uce58\ud55c\ub2e4. \ud2b9\ud788 \ubb38\uc7a5 \uc9d1\ud569\uc740 \ub9cc\uc871 \uac00\ub2a5\ud560 \ud544\uc694\ucda9\ubd84\uc870\uac74\uc5d0 \uc758\ud558\uc5ec \ubb34\ubaa8\uc21c\uc774\ub2e4.<\/p>\n<div class=\"contentbottombox\">\n<p class=\"contentbottomboxtitle\"><a href=\"\/blog\/invitation-to-mathematical-logic\/\">\uc9d1\ud569\uacfc \uc218\ub9ac\ub17c\ub9ac \uccab\uac78\uc74c \ubaa9\ucc28 \ubcf4\uae30<\/a><\/p>\n<p><span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch01-naive-logic\/\">\uba85\uc81c\uc640 \ub17c\ub9ac<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch02-sets\">\uc9d1\ud569\uc758 \uac1c\ub150<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch03-algebra-of-classes\">\ub2e4\uc591\ud55c \uc9d1\ud569\uc758 \uc5f0\uc0b0<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch04-relations-and-functions\">\uad00\uacc4\uc640 \ud568\uc218<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch05-infinite-sets\">\uc720\ud55c\uc9d1\ud569\uacfc \ubb34\ud55c\uc9d1\ud569<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch06-natural-numbers\">\uc790\uc5f0\uc218<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch07-cardinal-numbers\">\uc9d1\ud569\uc758 \uae30\uc218<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch08-ordinal-numbers\">\uc9d1\ud569\uc758 \uc11c\uc218<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch09-axiomatic-set-theory\">\uc9d1\ud569\ub860\uc758 \uacf5\ub9ac<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch10-axiom-of-choice\">\uc120\ud0dd \uacf5\ub9ac<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch11-formal-logic\">\ud615\uc2dd\ub17c\ub9ac<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch12-propositional-logic\">\uba85\uc81c\ub17c\ub9ac\uc758 \uac1c\ub150<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch13-soundness-completeness-proplogic\">\uba85\uc81c\ub17c\ub9ac\uc758 \uac74\uc804\uc131\uacfc \uc644\uc804\uc131<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch14-syntax-first-order-logic\">\uc77c\uacc4\ub17c\ub9ac\uc758 \uad6c\ubb38\ub860<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch15-semantics-first-order-logic\">\uc77c\uacc4\ub17c\ub9ac\uc758 \uc758\ubbf8\ub860<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch16-inference-rule-first-order-logic\">\uc77c\uacc4\ub17c\ub9ac\uc758 \ucd94\ub860\uaddc\uce59<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch17-compactness-first-order-logic\">\uc77c\uacc4\ub17c\ub9ac\uc758 \ucf64\ud329\ud2b8\uc131<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch18-peano-arithmetics\">\ud398\uc544\ub178 \uc0b0\uc220<\/a><\/span><br \/>\n<span class=\"contentboxindex\"><a href=\"\/blog\/invitation-to-mathematical-logic\/ch19-incompleteness-theorem\">\ubd88\uc644\uc804\uc131 \uc815\ub9ac<\/a><\/span>\n<\/div>\n<\/div>\n<p><!-- ################## --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>\uc774\uc81c \uc758\ubbf8\ub860\uacfc \ube44\uad50\ud560 \uc77c\uacc4\ub17c\ub9ac\uc758 \ud615\uc2dd\ucd94\ub860\uacc4\ub97c \uc815\ud55c\ub2e4. \uc774 \uc7a5\uc5d0\uc11c\ub294 \uac00\uc815\uc73c\ub85c \uc0ac\uc6a9\ud558\ub294 \ub17c\ub9ac\uc2dd\ub4e4\uc744 \ubb38\uc7a5\uc73c\ub85c \uc81c\ud55c\ud55c\ub2e4. \ub530\ub77c\uc11c \uc804\uce6d \uc77c\ubc18\ud654 \uaddc\uce59\uc744 \uc0ac\uc6a9\ud560 \ub54c \uc790\uc720\ubcc0\uc218\ub97c \uac00\uc9c4 \uac00\uc815 \ub54c\ubb38\uc5d0 \uc0dd\uae30\ub294 \ubd80\uac00\uc870\uac74\uc744 \ub530\ub85c \uc801\uc744 \ud544\uc694\uac00 \uc5c6\ub2e4. \uc790\uc720\ubcc0\uc218\ub97c \uac00\uc9c4 \uac00\uc815\uae4c\uc9c0 \ud5c8\uc6a9\ud558\ub824\uba74 \uc77c\ubc18\ud654\ub418\ub294 \ubcc0\uc218\uac00 \ubaa8\ub4e0 \ubbf8\ud574\uc81c \uac00\uc815\uc5d0\uc11c \uc790\uc720\ub86d\uac8c \ub098\ud0c0\ub098\uc9c0 \uc54a\ub294\ub2e4\ub294 \ud45c\uc900\uc801\uc778 \uc81c\ud55c\uc774 \ud544\uc694\ud558\ub2e4. \uba85\uc81c\ub17c\ub9ac\uc640 \ub9c8\ucc2c\uac00\uc9c0\ub85c \ub2e4\uc74c \uc138 \uacf5\ub9ac\ud2c0\uc744 \uc0ac\uc6a9\ud55c\ub2e4. (A1) \\(\\phi\\to(\\psi\\to\\phi)\\) (A2) \\((\\phi\\to(\\psi\\to\\theta))\\to((\\phi\\to\\psi)\\to(\\phi\\to\\theta))\\) (A3) \\((\\neg\\phi\\to\\neg\\psi)\\to(\\psi\\to\\phi)\\) \ud55c\uc815\uae30\ud638\ub97c \uc704\ud55c \uacf5\ub9ac\ud2c0\uc740 \ub2e4\uc74c\uacfc \uac19\ub2e4. (A4) \\((\\forall x)\\phi\\to\\phi[t\/x]\\),&hellip;<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":9246,"menu_order":116,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_lmt_disableupdate":"no","_lmt_disable":"","footnotes":""},"class_list":["post-9280","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/pages\/9280","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/comments?post=9280"}],"version-history":[{"count":17,"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/pages\/9280\/revisions"}],"predecessor-version":[{"id":10096,"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/pages\/9280\/revisions\/10096"}],"up":[{"embeddable":true,"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/pages\/9246"}],"wp:attachment":[{"href":"https:\/\/sasamath.com\/blog\/wp-json\/wp\/v2\/media?parent=9280"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}