stanford-oval/wikipedia huggingface dataset:
梁家傑
生平 > 外傭居港權爭議

在2011年的外傭居港權爭議中，梁家傑指《入境條例》附表已為「以香港為永久居住地」列出4個條件，即使外傭在司法覆核勝訴，絕大多數外傭也會因為不符合該4個條件而不會獲得永久居港權。梁家傑在一封公開信中指《入境條例》附表條件「包括有否在港納稅、有否在港持有物業、家庭成員是否在港等等」。自由黨主席劉健儀認為梁家傑所說的「四大關卡」與《入境條例》附表原文不符，批評梁家傑「偷換概念，指鹿為馬」及誤導市民。香港《文匯報》有評論批評梁家傑「故意以假資訊來誤導市民，令市民誤以為影響不大而掉以輕心，甚至原諒公民黨的“賣港”惡行」。
梁家傑因黨友李志喜為外傭打官司而備受批評，同時公民黨的支持度亦大跌。數年後受訪時，梁家傑解釋法律界有所謂的「驛站原則(cab-rank rule)」，像的士司機不能拒載一樣，行規是大律師不能隨便拒絕接案，否則一些特殊求助人將無法得到應有的法律支援。梁指出，外傭居港權案中有一些法律觀點需要釐清，這樣才對香港人及其他持份者公平，而全港擅長相關案件的大律師只有幾人，其中一位是公民黨的李志喜。梁的講法與前大律師公會主席林孟達的講法吻合。林在2012法律年度開啟典禮致辭時強調，當大律師出庭代表某方時，該名大律師只是在履行「驛站原則」，希望公眾理解。
生平 > 反修例运动期间

2019年7月18日举行的港大校長與學生論壇中，梁家傑发言时宣称“有時候暴力或可能是解決問題的方法”（violence may sometime be THE solution to a problem），引爆全场，但校长张翔在回应中即刻表示反对该主张。
生平 > 已解散或退出公民黨

2021年3月，公民黨原定創立15周年，公民黨騰出後的前黨魁楊岳橋、黨員副主席譚文豪、郭家麒及東區區議員李予信，因參與「35+47」個人初選案件被控串謀顛覆國家政權罪，現正被還柙，四人經已退出公民黨相繼辭職，剩下是公民黨主席梁家傑等。
2023年5月27日，下午宣佈公民黨清盤後解散，亦最後一個公民黨前成員。
學歷及專業資格

喇沙小學畢業
九龍華仁書院畢業
香港大學法律學士（1982年）
香港大律師（1983年）
英國劍橋大學休斯學院法律碩士（1984年）
香港資深大律師（1998年）
現任公職

市區重建局非執行董事（2005年5月 -）
雙語法律制度委員會委員（1997年 -）
投訴警方獨立監察委員會副主席（2005年1月 -）
應用研究局董事（2000年2月 -）
社會福利署暴力及執法傷亡賠償組組員（2000年6月 -）
香港大學法律學院法律專業教育系名譽講師（2000年9月 -）
水污染管制上訴委員會主席（2001年1月 -）
香港貿易發展局專業服務諮詢委員會委員（2002年1月 -）
歷任公職

香港大律師公會主席（2001年1月 - 2003年1月）
香港大律師公會內地執業及關係委員會主席（2000年－2004年）
香港特別行政區中央政策組非全職顧問（2000年－2002年）
檢討香港法律教育及培訓督導委員會委員（1999年－2002年）
香港特別行政區中央政策組社會凝聚力小組組員（2002年8月 - 2003年7月）
教育統籌局師訓與師資諮詢委員會初職教師見習評審專責小組主席（2003年）
投訴警方獨立監察委員會會員（2000年－2004年）
公民黨黨魁（2011年 - 2016年）
公民黨主席（2016年 - 2023年）
立法會議員（九龍東）（2004年10月 - 2016年9月）
家庭

梁已婚，妻子陳淑儀；育有一女兩子。
相關

九龍華仁書院
公民黨 (香港)
外部連結

梁家傑 Facebook（页面存档备份，存于）
香港立法會議員
Bar List at HKBA
梁家傑政制訪問:《領導者》2009年12月號（页面存档备份，存于）
梁家傑 追求公平 根深柢固（页面存档备份，存于）
| 政黨職務 |
| --- | --- | --- |
| 前任： 余若薇 |  公民黨主席 2016年－2023年 | 政党解散 |
| 前任： 余若薇 |  公民黨黨魁 2011年－2016年 | 繼任： 楊岳橋 |
| 前任： 張超雄 |  公民黨副主席（內務） 2008年－2011年 | 繼任： 吳靄儀 |
| 前任： 首任 |  公民黨九龍東支部主席 2006年－2008年 | 繼任： 余冠威 |
| 前任： 馮檢基 | 泛民會議召集人 2014年－2015年 | 繼任： 何秀蘭 |
| 0 | 1 | 2 |
| --- | --- | --- |

官衔
| 前任： 湯家驊 |  香港大律師公會主席 2001年 - 2002年 | 繼任： 陳景生 |
|  论 编2007年香港特別行政區行政長官選舉 |
| --- | --- |
正式候選人: (1) 梁家傑  ·  (2) 曾蔭權
其他參選人: 李永健  · 紀文珊  · 詹振榮
梁家傑2007年爭取2012真普選遊行
梁家傑（2016年）
梁家傑在五區公投爭取真普選大會上
梁家傑（攝於2013年）
攝於2023年5月27日，在公民黨成員清盤後的最後一任主席為梁家傑等。
梁家傑在2007年七一大遊行中為書籍「袋巾背後」簽名
巴黎的拱廊街

在19世纪上半叶，法国巴黎拱廊街（法語：）的数目曾达到150条，此后由于奥斯曼改造巴黎而大幅度减少，到21世纪仅存二十多条，全部分布在右岸。
现存拱廊街列表

| 区份  | 名称  | 建成年份  | 入口  | 开放时间  | 遗产名录编号  | 长度  | 图片  |
| --- | --- | --- | --- | --- | --- | --- | --- |
| 1 | Deux-Pavillons !Passage des Deux-Pavillons |  |  博若萊街（rue de Beaujolais）6号  小场街5号 |  | PA00085994 | 33m |  |
| 1 | Vero-Dodat !维侯多达拱廊街（Galerie Véro-Dodat） | 1826 |  让 - 雅克·卢梭街19号  Bouloi街2号 | 周一-周六 0700-2200 | PA00085995 | 80m |  |
| 2 | Ben-Aiad !Passage Ben-Aïad | 1826 |  9-11 rue Léopold-Bellan  8 rue Bachaumont |  | PA75020007 | 90m |  |
| 2 | Bourg-l'Abbe !布尔格拉贝拱廊街（Passage du Bourg-l'Abbé） | 1828 |  圣但尼街120号  Palestro街3号 | 周一-周六 0700-1900 | PA00086097 | 47m |  |
| 2 | Caire !开罗拱廊街（Passage du Caire） | 1798 |  亚历山大街33号  开罗广场2号  圣但尼街237-239号  开罗街14、34、44号 | 周一-周五 0700-1800 |  | 360m |  |
| 2 | Choiseul !舒瓦瑟尔拱廊街（Passage Choiseul） | 1829 |  小场街40号  圣奥古斯丁街23号  Dalayrac街40号  圣安娜拱廊街 |  | PA00086088 | 190m |  |
| 2 | Colbert !科尔伯特拱廊街（Galerie Colbert） | 1826 |  小场街6号  薇薇安街2号 |  | PA00086023 | 83m |  |
| 2 | Grand-Cerf !巨鹿廊街（Passage du Grand-Cerf） | 1825 |  圣但尼街145号  10 rue Dussoubs | 周一-周六 0800 - 2000 | PA00086089 | 117m |  |
| 2 | Panoramas !全景廊街（Passage des Panoramas） | 1800 |  圣马克街10号  蒙马特大道11号  薇薇安街38号  蒙马特街151号 | 0600-2400 | PA00086090 | 133m |  |
| 2 | Ponceau !蓬索拱廊街（Passage du Ponceau） | 1826 |  塞瓦斯托波尔大道119号  圣但尼街212号 | 周一-周五 8-9 |  | 92m |  |
| 2 | Princes !王子拱廊街（Passage des Princes） | 1860 |  意大利大道5号  黎塞留街97-99号 | 周一-周六 0800 - 2000 | PA00086091 | 80m |  |
| 2 | Sainte-Anne !圣安娜拱廊街（Passage Sainte-Anne） |  |  圣安娜街59-61号  舒瓦瑟尔拱廊街 |  | PA00086088 | 47m |  |
| 2 | Vivienne !薇薇安拱廊街（Galerie Vivienne） | 1823 |  小场街4号  薇薇安街6号  5 rue de la Banque | 0800 - 2000 | PA00086024 | 176m |  |
| 3 | Moliere !莫里哀拱廊街（Passage Molière） |  |  82 rue Quincampoix  圣马丁街157, 159, 161号 |  | PA00086230 | 46m |  |
| 3 | Vendome !旺多姆拱廊街（Passage Vendôme） | 1827 |  16 rue Béranger  共和国广场3号 |  周一-周五 0700 - 2000  周六 0800 - 2000 | PA00086231 | 57m |  |
| 6 | Commerce-Saint-Andre !圣安德雷商廊（Cour du Commerce-Saint-André） | 1776 |  59 rue Saint-André-des-Arts  21 rue de l'Ancienne-Comédie  130 boulevard Saint-Germain |  | PA00088654 | 120m |  |
| 8 | Berryer !Cité Berryer |  |  博伊斯-丹格拉斯街24号  皇家街24号 |  | PA00088811 | 95m |  |
| 8 | Lido !丽都商场（Arcades du Lido） | 1926 |  香榭丽舍大街76-78 号  59 rue de Ponthieu |  |  | m |  |
| 8 | Madeleine !马德莱娜拱廊街（Galerie de la Madeleine） | 1845 |  马德莱娜广场9号  30 rue Boissy-d'Anglas | 周一-周六 0800-1900 | PA00088815 | 53m |  |
| 8 | Puteaux !皮托拱廊街（Passage Puteaux） | 1839 |  33 rue de l'Arcade  28 rue Pasquier | 周一-周五 0700 - 2400 |  | 29m |  |
| 9 | Havre !杜哈佛拱廊街（Passage du Havre） | 1845 |  考马尔廷街69号  圣拉扎尔街109号 |  |  | 115m |  |
| 9 | Jouffroy !茹弗鲁瓦廊街 | 1845 |  蒙马特大道10-12号  9 rue de la Grange-Batelière | 0700 - 2100 | PA00088996 | 140m |  |
| 9 | Verdeau !韦尔多拱廊街（Passage Verdeau） | 1847 |  6 rue de la Grange-Batelière  蒙马特郊区街31号 |  周一-周五 0700 - 2100  周六-周日 0700 - 2000 | PA00088997 | 75m |  |
| 10 | Brady !布雷迪拱廊街（Passage Brady） | 1828 |  圣马丁郊区街43号  斯特拉斯堡大道22号  斯特拉斯堡大道33号  圣但尼郊区街46号 |  | PA75100007 | 216m |  |
| 10 | Prado !普拉多拱廊街（Passage du Prado） | 1830 |  圣但尼大道16号  圣但尼郊区街16号 | 0900 - 1900 |  | 120m |  |
参考

↑  . Paris.fr. Marie de Paris.   [10 March 2015]. （原始内容存档于2015年2月16日）.
. The Guardian.   [2015-04-22]. （原始内容存档于2020-07-29）.
. ParisInfo.   [2015-04-22]. （原始内容存档于2017-02-02） （法语）.
奧基喬比縣

| 奧基喬比縣 Okeechobee County |
| --- | --- |
县
County of Okeechobee
奧基喬比縣司法大廈
   圖章
 奧基喬比縣于佛罗里达州的位置
 佛罗里达州于美国的位置
坐标： 27°23′N 80°53′W﻿ / ﻿27.39°N 80.89°W﻿ / 27.39; -80.89
国家:  美国
州:  佛罗里达州
设立日期: 1917年5月8日
語源: 奧基喬比湖
县治: 奥基乔比
最大城市: 奥基乔比
面积
 • 总计: 892 平方英里（2,000 平方公里）
 • 陸地: 769 平方英里（2,000 平方公里）
 • 水域: 123 平方英里（300 平方公里）  13.8%
人口（2020年）
 • 總計: 39,644人
 • 密度: 52人/平方英里（20人/平方公里）
时区: 东部时区（UTC−5）
 • 夏时制: 东部时区（UTC−4）
郵區編號: 34972, 34973, 34974
电话区号: 863
包含的国会选区: 第17選區
網站: www.co.okeechobee.fl.us
奧基喬比縣（英語：）是美国佛罗里达州中南部的一個县。根据2020年美国人口普查数据，该县总人口为39,644人，县治设在奥基乔比市。奥基乔比县是奥基乔比小都会统计区的一部分，同时也是迈阿密-劳德代尔堡-圣露西港联合统计区的组成部分。
奥基乔比县于1917年5月8日正式成立，是佛罗里达州的第54个县。其名称来源于奥基乔比湖，"Okeechobee"一词源自塞米诺尔人的语言，意为“大水”，这一名称贴切地反映了该地区的自然特征。奥基乔比湖是美国第二大淡水湖，也是佛罗里达州最大的湖泊，为当地居民和游客提供了丰富的水上活动和生态旅游资源。奥基乔比市是该县唯一的建制城市，也是该县的政治、经济和文化中心。奥基乔比县总面积为892平方英里（约2,310平方公里），其中陆地面积为769平方英里（约1,990平方公里），水域面积占比约13.8%。该县地处佛罗里达腹地地区，东临圣露西县、马丁县和印第安河县，西邻高地县，西南方向接壤沼泽县和亨德里县，北部则与奥西欧拉县和波尔克县相连。该县的地理位置使其成为佛罗里达州中部与东南部地区的交通枢纽，同时也是农业和畜牧业的理想发展区域。
奥基乔比县以广阔的自然景观、丰富的农业资源以及世界级的钓鱼产业而闻名，当地经济主要依赖农业、畜牧业和渔业。该县长期以来是佛罗里达州奶牛和农业产业的重镇，以广袤的牧场和畜牧业闻名。全县约有65,000头肉牛，是佛罗里达州主要的畜牧地区之一。奥基乔比牲畜市场始建于1930年代，至今仍是佛罗里达州交易量最大的牲畜市场。此外，该县在佛罗里达州乳制品供应链中占有重要地位。除了农业和畜牧业，奥基乔比县还是世界著名的钓鱼胜地，被誉为“世界黑鲈之都”。奥基乔比湖每年吸引成千上万的垂钓爱好者，他们在这里体验湖泊丰富的鱼类资源，尤其是大口黑鲈的垂钓活动。
赫尔辛基市政厅

| 赫尔辛基市政厅 |
| --- | --- |
芬蘭語： 瑞典語：

曾用名: Hotel Seurahuone
概要
類型: 地方政府大樓[*]、建筑物
用途: 办公大楼[*]
所屬國家／地區: 芬兰
行政区: 赫尔辛基
地址: Pohjoisesplanadi 11、​Pohjoisesplanadi 11-13
: 60°10′05″N 24°57′10″E﻿ / ﻿60.1681°N 24.9529°E﻿ / 60.1681; 24.9529
邮政编码: 00170
现居租户: 赫尔辛基市
竣工日: 1833
翻新: 1965–70; 1985–88; 1998–99
设计与建造
建筑师: 卡尔·卢德维格·恩格尔（最初设计） 阿尔诺·鲁苏沃里（英语：）（翻新扩展）
保护情况: 城市规划上受保护的建筑[*]
地圖

赫尔辛基市政厅（芬蘭語：，瑞典語：）是芬兰赫尔辛基的市长办公室和市议会的一处会场，位于克鲁农哈卡区，毗邻赫尔辛基集市广场，地址为Pohjoisesplanadi 11-13号。
历史

该建筑完成于1833年，原为Hotel Seurahuone，是一个重要的文化设施。酒店由卡尔·卢德维格·恩格尔设计，他还设计了附近元老院廣場周边的主要建筑。该市在1901年购买了这座建筑，1913年酒店搬迁后，更新为市政厅。
1965年至70年间，在一场建筑设计竞赛之后，市政厅由建筑师阿尔诺·鲁苏沃里（英语：）进行了彻底的改造，取代了许多古老的古典内饰，兴建了现代的玻璃幕墙。
1908年时的建筑
1980年代扩建的部分
2018年赫尔辛基自豪游行时的市政厅
该建筑还为赫尔辛基居民和移民提供公共信息服务，举办展览，音乐会和电影放映。
参考

1 2  . City of Helsinki.   [2014-07-02]. （原始内容存档于2014-07-14）.
↑  . City of Helsinki / University of Helsinki.   [2014-07-02]. （原始内容存档于2014-12-16）.
一阶逻辑

一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统，也可以稱為：一阶斷言演算、低階斷言演算、量化理論或谓词逻辑。一階邏輯和命題邏輯的不同之處在於，一階邏輯包含量詞。
高階邏輯和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞。在一階邏輯的語義中，斷言被解釋為關係。而高階邏輯的語義裡，斷言則會被解釋為集合的集合。
在通常的語義下，一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）的。雖然一階邏輯的邏輯歸結只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯（英语：）定理，如勒文海姆–斯科倫定理及緊緻性定理。
一階邏輯是數學基礎中很重要的一部份。許多常見的公理系統，如一階皮亞諾公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗蘭克爾集合論都是一階理論。然而一階邏輯不能控制其無窮模型的基數大小，因根據勒文海姆–斯科倫定理和康托爾定理，可以構造出一種“病態”集合論模型，使整個模型可數，但模型內卻會覺得自己有「不可數集」。類似地，可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論。但一階的直覺主義邏輯裡，勒文海姆–斯科倫定理不可證明，故不會有以上之現象。
簡介 > 基本符號

命題邏輯顧名思義，會將「蘇格拉底是哲學家」、「柏拉圖是哲學家」之類直觀上有真有假的敘述簡記為  p 及  q （也就是有真有假的命題），然後討論  \neg p（非p）、 p\Rightarrow q（若p則q）、 p\wedge q（p且q）與 p\vee q（p或q）之間的推理關係。
但一階邏輯嘗試從一些比較基礎的詞彙去建構「句子」，比如說，可用符號  {\text{Phil}}(x) 代表 「 x 是哲學家」，也就是賦予斷言符號「 {\text{Phil}}(x) 」語意的解釋。這個解釋預設一個「所有人類的群體」（也就是下面標準語義一節會說到的论域），并將變數  x 對應為自群體中取出來的某人。
以此類推，斷言符號可以包含一個以上的變數。例如：可以將  {\text{Cp}}(x,\,y) 解釋為「 x 與 y 是夫妻」。
一階邏輯類似於命題邏輯，可以將斷言符號與  \neg （非）、 \Rightarrow （則）、 \wedge （且）和  \vee （或）組成更複雜的敘述，例如：把斷言符號  {\text{Schol}}(x) 解釋成「  x 是學者」，那「若 x 為哲學家，則 x 為學者」可表示為：
但相較之下，一階邏輯又加入了描述「所有」與「存在」的量詞，比如說「對所有 x ，若 x 為哲學家，則 x 為學者」可記為：
也就是自左方開始閱讀，將  \forall x 解釋成「对所有 x 有…」。 \forall  這個符號被称为全稱量詞。
而對於「有 x 是哲學家」这一叙述，一階邏輯則引入另一種量詞：
也就是自左方開始閱讀，將  \exists x 解釋成「存在  x 使…」。 \exists  這個符號被称为存在量詞。
順帶一提「並非所有 x 不是哲學家」等價於「有 x 是哲學家」；且「不存在 x 不是學者」也等價於「所有的 x 是學者」。所以可以用「否定」和「全稱量詞」來組合出「存在量詞」。換句話說，可作以下的符號定義（ {\mathcal {A}} 代表一段「敘述」）：
簡介 > 相等

一階邏輯也考慮到「相等」這個概念在敘述中的重要性，例如想表達「若所有 x是哲學家，那 x的長子也會是哲學家」，可先把  {\text{Son}}(x) 解釋為 「 x 的長子」，那么這段敘述可記為：
換句話說， {\text{Son}}(x) 被解釋成「與  x 有特定且唯一對應關係」的某對象（被稱為函數符號）。換句話話說，只要「 x就是 y」，那「 x的長子也會是 y的長子」。換句話說：
這些性質被一階邏輯視為「理所當然」。
類似地，敘述中也有一些「不變的實體」，如苏格拉底，表示這些「實體」的符號被稱為常數符號。例如將  s 解釋為苏格拉底，那「苏格拉底為哲學家」就可以寫成：
所謂的「不變」隱含的代表：
換句話說
這兩個性質也被一階邏輯視為「理所當然」。
形式理論

一階邏輯的形式理論可分成幾個部份：
語法（英语：）：決定哪些符號組合是合式公式。（直觀上的“文法無誤的敘述”）
推理規則：由合式公式符號組合出新合式公式的規則（直觀上的“推理”）
公理：一套合式公式（直觀上的基本假設）
形式理論 > 基本符號

一套理論能容許多少符號，取決於人類能運用物理定律來塑造多少符號，但目前無法確知宇宙是不是有限，或是以可無限制地分割。雖然所有的公理化集合論都以量詞的形式隱晦的承認跟自然數一樣多的無窮（如ZF集合論的無窮公理），甚至以這樣的可數無窮為基礎，去建構出不可數的實數，但將抽象的理論對應到現實時，還是需要回答物理上有沒有可數或不可數的無窮。所以謹慎起見，如果沒有特別申明的話，以下各種類符號的數目上限都是有限的。
形式理論 > 基本符號 > 邏輯符號

一階邏輯通常擁有以下的符號：
量化符號 \forall 及 \exists
某些作者會把  \exists  符號定義為  \exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]，如此便只需要  \forall  做為基礎符號。
邏輯聯結詞：以下為可能的表示符號（关于波蘭表示法下的邏輯連接詞，請參見逻辑运算的波兰记法）： {\mathcal {A}}\wedge {\mathcal {B}}:=\neg ({\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})), {\mathcal {A}}\vee {\mathcal {B}}:=(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}}, {\mathcal {A}}\Leftrightarrow {\mathcal {B}}:=({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}}), 如此一來只需要否定和條件做為基礎符號。
否定：  \neg  或  \sim  或－
條件： \Rightarrow  或  \rightarrow  或  \supset
且： \land  或  \&
或： \lor  或 ||
雙條件： \Leftrightarrow  或  \leftrightarrow
某些作者會作如下的符號定義：
標點符號：括號、逗號及其他，依作者的喜好有所不同。
為了更有效的將括號做配對，通常還會採用大括號{  }跟中括號[  ]。
至多跟自然數一樣多的變數，通常標記為英文字母末端的小寫字母x、y、z、…，也常會使用下標（或上標、上下標兼有）來區別不同的變數：x0、x1、x2、…（特別注意c有時候會被當成常數符號而引起混淆）。
等式符號： =
有作者會因為語義上对“相等”的不同解释，而將等式符號視為雙元斷言符號、甚至是某種合式公式的簡寫。
符號相等： \asymp
某些作者會額外採用這個符號來表示符號辨識上的等同以便與等式符號作區別。
並非所有的符號都不可或缺的，像謝費爾豎線「 |」（或異或）可以用來定義量詞以外的所有邏輯符號，換句話說：
符號定義 — 

 (\neg {\mathcal {A}}):=({\mathcal {A}}|{\mathcal {A}})
({\mathcal {A}}\Rightarrow {\mathcal {B}}):={\mathcal {A}}|({\mathcal {B}}|{\mathcal {B}})
({\mathcal {A}}\wedge {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {B}})|({\mathcal {A}}|{\mathcal {B}})\,]
({\mathcal {A}}\vee {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {A}})|({\mathcal {B}}|{\mathcal {B}})\,]
另外，一些作者不區分語義解釋和形式理論，所以會將表示真值的符號納入形式理論裡，也就是說，用 T 、Vpq 或  \top  來表示「真」，並用 F 、 Opq 或  \bot  來表示「假」。
形式理論 > 基本符號 > 斷言符號

「他們兩人是夫妻」，是一個關於兩個“對象”的斷言，而「他是人」、「三點共線」则表明斷言容許一個或者多個對象。所以對於自然數  n  、 j 約定：
為一階邏輯的合法詞彙。它在直觀上表示一個有  n 個“對象”的斷言，稱為  n 元斷言符號。下標的自然數  j 只是拿來和其他同為  n 元的斷言符號作區別。
實用上只要有申明，不至於和其他詞彙引起混淆的話，可以用任意的形式簡寫一個斷言符號。如：公理化集合論裡的雙元斷言符號  A_{1}^{2}(x,\,y) 也可以表示为  x\in y 。
形式理論 > 基本符號 > 函數符號

「物體的顏色」、「夫妻的長子」这种断言說明了一组對象所唯一對應的對象。但不同的夫妻有不同的長子；不同的物體有不同的顏色。據此，形式上對於自然數  n  、 j  約定：
為一階邏輯的合法詞彙，直觀上表示  n 個“對象”所對應到的東西，稱它為  n 元函數符號。需要特別注意，這種“唯一對應”的直觀想法，必須配上關於“等式”的性質（詳見下面的等式定理章节），才能在形式理論中被實現。
与斷言符號一样，只要不引起混淆，就可以用任何的形式簡寫函數符號。如：公理化集合論裡的  x\cup y 是依據聯集公理而定義的新函數符號（請參見下面函數符號與唯一性章節），也可以冗長的表記為  f_{j}^{2}(x,\,y) 。
形式理論 > 基本符號 > 常數符號

「刻度0」、「原點」、「蘇格拉底」是直觀上＂唯一不變＂的對象。據此，對自然數  j 約定
為一階邏輯的合法詞彙，直觀上表示一個“唯一不變”的對象，稱為常數符號。同樣的。“常數的不變性”需配上等式的性質（詳見下面等式定理）才能被實現。
為了不和變數的表記混淆，常數符號一樣可以用任何的形式簡寫，如公理化集合論裡的  \varnothing  是根據空集公理和函數符號與唯一性，而定義的新常數符號。亦可冗長的表示為  c_{j} 。
形式理論 > 語法

和自然語言（如英語）不同，一階邏輯的語言以明確的遞迴定義判斷一個給定的詞彙是否合法。大致上來說，一階邏輯以「項」代表討論的對象，而對「項」的斷言組成了最基本的原子（合式）公式；而原子公式和邏輯符號組成了更複雜的合式公式（也就是“敘述”）。
形式理論 > 語法 > 項

「那對夫妻的長子的職業」、「 (x+y)\times z」、「 x\cup \varnothing 」代表變數可以與函數符號組成更一般的物件。據此形式，遞迴地規定一類合法詞彙——項為：
遞迴定義 —
變數和常數是項。
若  T_{1},\,....,\,T_{n} 全都是項，那么  f_{j}^{n}(T_{1},\,....,\,T_{n}) 也是項。
項只能通过以上兩點，於有限步驟內建構出來。
習慣上以大寫的西方字母（如英文字母、希伯來字母、希臘字母）代表項，如果變數不得不採用大寫字母，而可能跟項引起混淆的話，需額外規定分辨的辦法。
形式理論 > 語法 > 原子公式

為了比較簡潔地規定甚麼是合式公式，先規定原子公式為：（若  T_{1},\,....,\,T_{n} 是項）
這樣的形式。
形式理論 > 語法 > 公式

一階邏輯的合式公式（簡稱公式或  wf ）以下面的規則遞迴地定義：
遞迴定義 —
原子公式為公式。（美觀起見，在原子公式外面包一層括弧也是公式）
若  {\mathcal {A}} 為公式，則  (\neg {\mathcal {A}}) 為公式。
若  {\mathcal {A}} 與  {\mathcal {B}} 為公式，則  ({\mathcal {A}}\Rightarrow {\mathcal {B}}) 為公式。
若  {\mathcal {A}} 為公式，  x 為任意變數，則  (\forall x{\mathcal {A}}) 為公式。 （美觀起見  (\forall x){\mathcal {A}}:=\forall x{\mathcal {A}}，也就是裡面的量詞有無外包括弧都是公式）
合式公式只能通过以上四點，於有限步驟內建構出來。
另外成對的中括弧跟大括弧，符號辨識上視為成對的小括弧，而草書的大寫西方字母為公式的代號。
舉例來說，
是公式而
則不是公式。
而接下來只要對任意公式 {\mathcal {A}} 、  {\mathcal {B}} 與變數  x，做以下符號定義
符號定義 — 

 ({\mathcal {A}}\wedge {\mathcal {B}}):=\{\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]\}
({\mathcal {A}}\vee {\mathcal {B}}):=[(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]
({\mathcal {A}}\Leftrightarrow {\mathcal {B}}):=[({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}})]
(\exists x{\mathcal {A}}):=\{\neg [\forall x(\neg {\mathcal {A}})]\} （同樣美觀起見  (\exists x){\mathcal {A}}:=\exists x{\mathcal {A}}）
這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。
形式理論 > 語法 > 施用

所謂的施用/作用，是以下公式形式的口語說法：（其中  {\mathcal {A}} 與  {\mathcal {B}} 都是公式）
(\neg {\mathcal {A}}) 稱為  \neg  施用於  {\mathcal {A}} 上。
({\mathcal {A}}\Rightarrow {\mathcal {B}}) 稱為  \Rightarrow  施用於  {\mathcal {A}} 和  {\mathcal {B}} 上。
({\mathcal {A}}\wedge {\mathcal {B}}) 稱為  \wedge  施用於  {\mathcal {A}} 和  {\mathcal {B}} 上。
({\mathcal {A}}\vee {\mathcal {B}}) 稱為  \vee  施用於  {\mathcal {A}} 和  {\mathcal {B}} 上。
({\mathcal {A}}\Leftrightarrow {\mathcal {B}}) 稱為  \Leftrightarrow  施用於  {\mathcal {A}} 和  {\mathcal {B}} 上。
(\forall x{\mathcal {A}}) 稱為  \forall x 施用於  {\mathcal {A}} 上。
(\exists x{\mathcal {A}}) 稱為  \exists x 施用於  {\mathcal {A}} 上。
就类似于運算子作用在它們身上。
形式理論 > 語法 > 自由變數和約束變數

量詞所施用的公式被稱為量詞的範圍（scope）。同一個變數在公式一般來說不只出現一次，若變數  x 出現在  \forall x 的範圍內，稱這樣出現的  x 為不自由/被約束的  x （not free/bounded）；反過來說，不出現在  \forall x 的範圍內的某個  x 被稱為自由的  x。
例如，對於公式：
[A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)] 就是量詞   \forall x  的範圍；而  A_{1}^{1}(x) 裡的  x 就是不自由的；反之  A_{2}^{1}(y) 裡的  y 就是自由的。
說  x 於公式  {\mathcal {A}} 完全自由，意為於  {\mathcal {A}} 出現的  x 都是自由的；反之，說  x 於公式  {\mathcal {A}} 完全不自由/完全被約束，意為  {\mathcal {A}} 內根本沒有  x ，或是  {\mathcal {A}} 內沒有自由的  x 。若  {\mathcal {A}} 內所有的變數都完全不自由， {\mathcal {A}} 特稱為封閉公式/句子（closed formula/sentence）。
形式理論 > 語法 > 括弧的簡寫

括弧是為了保證語意解釋符合預期，但太多的括弧書寫不易，為此規定以下的“重構法”（反過來就是“簡寫法”），從表面上不合法的一串符號找出作者原來想表達的公式：
若整串符號的括弧不成對，直接視為無法重構。
以 \lnot ,\,\land ,\,\lor ,\,\forall ,\,\exists ,\,\Rightarrow ,\,\Leftrightarrow （左至右）的施用順序重構括弧。
相鄰的邏輯連接詞或量詞無法決定施用順序的話，以右邊為先。
重構施用的順序，以被成對括弧包住的部分為優先施用，其次才是落單的斷言符號。
舉例來說
的重構過程如下
\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \exists x[\lnot A_{2}^{1}(x)] （優先施用  \lnot ）
\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\} （施用  \exists ）
\{\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}\} （最後施用  \Rightarrow ）
可以被重構為公式的一串符號則寬鬆的認定為“合式公式”。（最明顯的例子就是合式公式最外層的括弧可以省略）
形式理論 > 語法 > 波蘭表示法

波蘭表示法將邏輯連接詞前置於被施用的公式而非傳統的中間。如果沿用以上的＂施用順序＂，這個表示法允許捨棄所有括弧。如公式
轉成波蘭表示法的過程如下
形式理論 > 推理规则

一階邏輯通常只有以下的推理規則（因為將普遍化視為推理規則會有不直觀的限制）
MP律 — 對於公式  {\mathcal {A}} 和  {\mathcal {B}} 有
直觀意義非常明顯，就是p=>q且p可以推出q。
在只以謝費爾豎線「 |」為基礎邏輯連接詞的公理系统裡，MP律會被改寫成
修改的MP律 — 對於公式  {\mathcal {A}} 、 {\mathcal {B}} 和  {\mathcal {C}} 有
 {\mathcal {A}}|({\mathcal {C}}|{\mathcal {B}}) 和  {\mathcal {A}} 組合出  {\mathcal {B}}。
形式理論 > 公理 > 邏輯公理

公理 — 如果 {\mathcal {B}}、 {\mathcal {C}}、 {\mathcal {D}}都是公式，則：
（A1）  {\mathcal {B}}\Rightarrow ({\mathcal {C}}\Rightarrow {\mathcal {B}})
（A2）  [{\mathcal {B}}\Rightarrow ({\mathcal {C}}\Rightarrow {\mathcal {D}})]\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {C}})\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {D}})]
（A3）  [(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})]\Rightarrow [(\neg {\mathcal {B}}\Rightarrow {\mathcal {C}})\Rightarrow {\mathcal {B}}]
都是公理。
它们实际上是公理模式，代表著“跟自然數一樣多”條的公理。
在有（A1）與（A2）的前提下，（A3）等價於以下的公理模式：（證明請參見下面否定一節。）
（T1） —  [\,(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})\,]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})
另外，在只以謝費爾豎線「 |」為基礎邏輯連接詞的公理系统裡，上面三條公理模式等價於下面這條公理模式：
公理 — 如果  {\mathcal {B}}、 {\mathcal {C}}、 {\mathcal {D}} 、 {\mathcal {E}} 和  {\mathcal {F}} 都是公式，則：
[\,{\mathcal {B}}|({\mathcal {C}}|{\mathcal {D}})\,]|{\big \{}\,[\,{\mathcal {E}}|({\mathcal {E}}|{\mathcal {E}})\,]|\{\,({\mathcal {F}}|{\mathcal {C}})|[\,({\mathcal {B}}|{\mathcal {F}})|({\mathcal {B}}|{\mathcal {F}})\,]\,\}\,{\big \}}
都是公理。
形式理論 > 公理 > 量词公理

公理 —  x 為任意變數，  {\mathcal {B}} 、  {\mathcal {C}} 為任意公式，則
（A4）  T 是一個項，  t 為  T 中出現的任意變數；若  {\mathcal {B}} 裡，自由的  x 都不在  \forall t 的範圍裡（這樣取代成  T 時才不會被  \forall t 約束），則
（A5）如果  x 在  {\mathcal {B}} 裡完全被約束，則
（A6）  [(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Rightarrow [(\forall x{\mathcal {B}})\Rightarrow (\forall x{\mathcal {C}})] 為公理
（A7） 若  {\mathcal {B}} 是公理，  x 是任意變數，則
它们实际上也是公理模式。
形式理論 > 公理 > 等式和它的公理

根據不同作者的看法，甚至是理論本身的需求，「等式」在形式理論裡可能是斷言符號或是一段公式（如 a 等於 b 可定義為對所有的 x ， x 屬於 a 等價於 x 屬於 b ）。而如何刻劃直觀上「等式的性質」，有一開始就將「等式的性質」視為公理（模式），但也有視為元定理的另一套處理方法，以下暫且以公理模式的方式處理。以元定理處理的方法會在等式定理詳述。
公理 —  (x=y) 是一段變數  x 、  y 完全自由，且型式完全被確定的公式  {\mathcal {E}}(x,\,y) 的簡寫。要求：
（E1）  (\forall x)(x=x) 為公理。
（E2） 若在公式  {\mathcal {A}} 中自由的  x 都不在  \forall y 的範圍內，以 {\mathcal {A}}_{y} 代表  {\mathcal {A}} 某些（而非全部）自由的  x  被取代成  y 而成的新公式，則
事實上這兩個公理模式也確保了函數符號“唯一對應”和常數符號的“唯一性”，但證明這些性質需要一些元定理，簡便起見合併於下面的等式定理一節講述。
標準語義

一階邏輯的標準語義源於波蘭邏輯學家阿尔弗雷德·塔斯基所著《On the Concept of Truth in Formal Languages》。根據上面語法一節，公式是由原子公式遞迴地添加邏輯連結詞而來的，而原子公式是由斷言符號與項所構成的。所以要檢驗一條公式在特定的論域下正不正確，就要規定項的取值，然後檢驗這樣的取值會不會落在斷言符號所對應的關係裡。由此延伸出所有公式的“真假值”。
也就是一套一階邏輯的語義解釋，要包含
變數取值的論域
如何解釋函數符號（為論域中的某個函數）與常數符號（為論域中的某特定元素），以便從特定的變數取值得出項的取值。
如何將斷言符號與論域裡的某關係做對應。
通常一套解釋方法（簡稱為解釋）會以代號  M 表示。
標準語義 > 項的取值

量詞的解釋需要指明變數取值範圍的論域——也就是一個集合  D 。而變數可能跟自然數一樣多，換句話說，所有變數在論域  D 取的值可以依序以自然數標下標——也就是一個在  D 取值的數列。如果以  x_{1},\,x_{2},\,x_{3},\,\cdots  的代號（不一定是變數本身的表示符號）來列舉變數，那麼從  D 的某套變數取值就以
或較直觀的符號
來表示。
一套解釋  M 會將  n 元函數符號  f_{i}^{n} 解釋成某個  {(f_{i}^{n})}^{M}:D^{n}\to D 的  n 元函數；而常數符號  c_{l} 解釋成特定的  {c_{l}}^{M}\in D （亦稱為  c_{l} 的取值為  {c_{l}}^{M}），這樣就可以用上面語法一節定義項的方式，遞迴地規定項的取值：
元定義 — 在解釋  M 下的某套變數取值下，一列項  T_{1},\,\cdots ,\,T_{n} 的取值分別為  {T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M}，則這套變數取值下，項  f_{i}^{n}(T_{1},\,\cdots ,\,T_{n}) 的取值規定為
標準語義 > 真假的賦值

直觀上要解釋關係最直接的方法，就是列舉所有符合關係的對象；例如如果想說明夫妻關係，可以列舉所有（老公, 老婆）的雙元有序對，但並非所有的人類有序對都會在這個關係中。
以此為基礎，若以  D^{m}  代表所有以  m 個  D 中的元素構成的  m 元有序對的集合（也就是  m 元笛卡兒積） ，那一套解釋  M 會將  m 元斷言符號  A_{j}^{m} 解釋為一個
的 m 元有序對子集合。
這樣就可以依據語法的遞迴定義，以下面的規則對每條公式賦予真值。（這種賦值方式稱為T-模式，取名於邏輯學家阿尔弗雷德·塔斯基）
元定義 — 在一套解釋  M 下：
在一套特定的變數取值下，一列項  T_{1},\,\cdots ,\,T_{m} 的取值為  {T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M} ，那  A_{j}^{m}(T_{1},\,\cdots ,\,T_{m}) 為真定義為
在一套特定的變數取值下，「 (\neg {\mathcal {B}}) 為真」 等價於 「 {\mathcal {B}} 為假」。
在一套特定的變數取值下， ({\mathcal {B}}\Rightarrow {\mathcal {C}}) 為真，意為「  {\mathcal {B}} 為假或是  {\mathcal {C}} 為真。」 （p=>q為假只有p為真且q為假的狀況）
在變數取值  \left\langle a_{k}\right\rangle _{k\in \mathbb {N} } 下， (\forall x_{i}{\mathcal {B}}) 為真，意為「對所有的  d\in D ，  {\mathcal {B}} 於變數取值  \left\langle a_{1},\,\cdots ,\,a_{i-1},\,d,\,a_{i+1},\,\cdots \right\rangle  下為真」。（也就是把變數  x_{i} 的取值換為論域的任意元素仍然為真）
更進一步的來說
元定義 — #在一套解釋  M 下，不管怎麼樣的變數取值，公式  {\mathcal {B}} 都為真，則稱為  M 下  {\mathcal {B}} 為真，以符號  M\vDash {\mathcal {B}} 簡記。若沒有變數取值可以滿足  {\mathcal {B}} ，則稱  M 下  {\mathcal {B}} 為假。
若任意解釋下公式  {\mathcal {B}} 都為真，稱  {\mathcal {B}} 為邏輯有效的（logically valid） （類似於命題邏輯的恆真式）
若一階邏輯理論  {\mathcal {L}} 的公理都於  M 為真，稱解釋  M 為  {\mathcal {L}} 之模型（model）
標準語義 > 代數化語義

另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆-塔斯基代數擴展而成。有如下幾種類型：
圓柱代數，由阿爾弗雷德·塔斯基和其同事提出；
多元代數，由保羅·哈爾莫斯提出。
斷言函子邏輯，主要是基於威拉德·范·奧曼·奎因的工作成果。
這些代數都是純粹擴展兩元素布林代數而成的格。
塔斯基和葛范德於1987年證明，沒有超過包在三個以上的量化內的原子句子的部份一階邏輯，其表示力和關係代數相同。上述部份一階邏輯令人十分地感到有興趣，因為它已足夠表示皮亞諾算術和公理化集合論，包括典型的ZFC。他們亦證明了，具有簡單有序對的一階邏輯和具有兩個有序的投影函數的關係代數等價。
標準語義 > 空論域

条目：空論域
上述的語義解釋都要求論域為非空集合。但在如自由邏輯之中，設定空論域是被允許的。甚至代數結構的類包含一個空結構（如空偏序集），當允許空論域時，這個類只能是一階邏輯中的一個基本類，不然就要將空結構由類中移除。
不過，空論域存在著一些難點：
許多常見的推理規則只在論域被要求是非空時才為有效的。一個例子為，當x不是 \phi \,內的自由變數時， \phi \lor \exists x\psi 會薀涵 \exists x(\phi \lor \psi )。這個用來將公式寫成前束範式的規則在非空論域中是可靠的，但在允許空論域時則是不可靠的。
在使用變數賦值函數的解釋中，真值的定義不能和空論域一起運作，因為不存在範圍為空的變數賦值函數。（相似地，也無法將解釋賦予上常數符號。）在甚至是原子公式的真值可被定義之前，都必須選定一個變數賦值函數。然後一個句子的真值即可在任一個變數賦值之下定義出其真值，且可證明其真值不依選定的賦值而變。這個做法在賦值函數不存在時不能運作；除非將其改成配上空論域。
因此，若空論域是被允許的，通常也必須被視成特例。不過，大多數的作家會簡單地將空論域由定義中排除。
常用的推理性質 > 定理與證明

以下介紹一些基本用語和符號
元定義 — 在一階邏輯理論  {\mathcal {L}} 下，   \vdash _{\mathcal {L}}{\mathcal {A}} 代表有一列公式  {\mathcal {C}}_{i}\,\,(1\leq i\leq n) 滿足：
{\mathcal {C}}_{n} 符號辨識上為  {\mathcal {A}}。
所有的  {\mathcal {C}}_{k}有下列兩種可能情況
{\mathcal {C}}_{k} 為  {\mathcal {L}} 的公理。
存在  i,\,j<k使得  {\mathcal {C}}_{i} 為  ({\mathcal {C}}_{j}\Rightarrow {\mathcal {C}}_{k}) （也就是由前面的公式以MP律組合出來）
口語上會稱公式  {\mathcal {A}} （或  \vdash _{\mathcal {L}}{\mathcal {A}} ） 為  {\mathcal {L}} 下的定理（theorem）。而這列 {\mathcal {C}}_{i}\,\,(1\leq i\leq n) 會稱為 \vdash _{\mathcal {L}}{\mathcal {A}} 的證明。
例如定理 (I)  \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {B}} 的證明：
證明 —
以上其實是蘊含了無限多定理的元定理的證明(因為沒有給出合式公式的明確形式)。方便起見，這種元定理還是會稱為定理並以同樣的形式來表達。
直觀上的證明，總是會有一些“前提假設”，對此，若以  \Gamma  代表一列有限數目的公式，那
元定義 —  \Gamma \vdash _{\mathcal {L}}{\mathcal {A}} 代表有一列公式  {\mathcal {C}}_{i}\,\,(1\leq i\leq n) 滿足：
{\mathcal {C}}_{n} 符號辨識上為  {\mathcal {A}}。
所有的  {\mathcal {C}}_{k} 有下列三種可能情況
{\mathcal {C}}_{k} 為  {\mathcal {L}} 的公理。
{\mathcal {C}}_{k} 為  \Gamma  中的其中一條公式。
存在  i,\,j<k使得  {\mathcal {C}}_{i} 為  ({\mathcal {C}}_{j}\Rightarrow {\mathcal {C}}_{k}) （也就是由前面的公式以MP律組合出來）
這樣稱  {\mathcal {C}}_{i}\,\,(1\leq i\leq n) 為在前提  \Gamma  下，  {\mathcal {A}} 的證明；或是說  {\mathcal {A}} 是  \Gamma  的推論結果。
若要特別凸顯  \Gamma  裡的一條＂前提條件＂  {\mathcal {B}} 對＂證明過程＂的重要性，可以用  \Gamma ,\,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {A}} 的符號去特別凸顯。若  \Gamma  裡的公式列舉出來有  {\mathcal {B}}_{1},...,{\mathcal {B}}_{n} ，那亦可表示為
證明過程沒有被引用的公式盡可能不寫出來。另一方面從以上對於證明定義可以發現，依怎樣的順序列舉前提條件，對於證明本身是不會有任何影響的。
本節所介紹的符號，在引用哪個理論很顯然的情況下， \vdash _{\mathcal {L}} 的下標 {\mathcal {L}} 可以省略。
實際的證明常常會＂引用＂別的（元）定理，嚴格來說，就是照抄（元）定理的證明過程，然後作一些修改使符號一致。為了節省證明的篇幅，引用時只會單單列出配合引用（元）定理所得出的公式（形式），並在後面註明引用的（元）定理代號。
常用的推理性質 > 演繹元定理

從公理（A1）和（A2）會得出不但直觀且實用的演繹元定理：
元定理 — 

一階邏輯理論  {\mathcal {L}} 下，若有  \Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}} ，則有  \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}
因為  \Gamma  代表的是有限條公式，所以透過演繹元定理可以將證明過程必要的前提條件遞迴地移到  \vdash  後，直到不需要任何前提為止；然後由MP律可以知道，若有  \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}} ，則有  \Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}，如此一來透過演繹元定理搬到推論結果的合式公式，也可以任意的搬回來。所以  \Gamma \vdash _{\mathcal {L}}{\mathcal {B}} 等價於某定理  \vdash _{\mathcal {L}}{\mathcal {C}} 。因此也會將  \Gamma \vdash _{\mathcal {L}}{\mathcal {B}} 稱為一個定理。
而從演繹元定理和MP律，會有以下直觀且實用的元定理
元定理 — 

（D1）  {\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{2},\,{\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}
（D2）  {\mathcal {D}}_{1}\Rightarrow ({\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}),\,{\mathcal {D}}_{2}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}
以下如果需要將引用的定理以演繹元定理進行＂搬移＂，會省略掉搬移的過程並在搬移後得到的結果後標註（D）。如果引用以上的（D1）和（D2）也會省略過程，單有結果和代號標註。