元逻辑
指研究形式逻辑系统逻辑演算命题演算是语义一致的，命题演算中的定理都是重言式；（二） 命题演算是语法一致的，并非任一公式都是命题演算的定理，如P∧q就不是系统中的定理；（三） 命题演算是在古典意义下一致的，对任一公式A, A和乛A不能都是命题演算定理。命题演算满足完全性的要求，即命题演算系统能够把所有的重言式推演出来。命题演算的完全性定理有两种表述方式：（一） 命题演算是在古典意义下完全的，一切重言式在命题演算中都是可证的；（二） 命题演算是语法完全的，如果把一不可证公式作为公理，其结果是系统不再具有一致性。但是命题演算不满足这样定义的完全性的要求：一公理系统是完全的，当且仅当对于任一公式A，或者A是可证的，或者乛A是可证的。例如，让A表示P∨q，则A和乛A在系统中都是不可证的。命题演算中的任一公式都是可判定的。对于任一命题公式A，都有能行的方法，即每一步都是由某个事先给定的规则明确规定了的并且在有穷步骤内可以完成的方法，来判定它是否重言式，是否系统中的定理。能行的方法有两种， 一种是真值表的方法，一种是范式的方法。元逻辑对谓词演算系统的研究取得下面的成果：谓词演算满足一致性的要求，即谓词演算系统自身是协调的、无矛盾的，谓词演算的一致性定理有两种表述方式：（一） 一阶谓词演算是在古典的意义下一致的，即不可能有一公式A, A和乛A都在系统中可证；（二） 一阶谓词演算是语法一致的，即有一公式A,A在系统中是不可证的。从一致性定理出发，可以引出两个有效性定理：（一） 对任一给定的整数K二命题演算是语法一致的，并非任一公式都是命题演算的定理，如P∧q就不是系统中的定理；（三） 命题演算是在古典意义下一致的，对任一公式A, A和乛A不能都是命题演算定理。
命题演算满足完全性的要求，即命题演算系统能够把所有的重言式推演出来。命题演算的完全性定理有两种表述方式：（一） 命题演算是在古典意义下完全的，一切重言式在命题演算中都是可证的；（二） 命题演算是语法完全的，如果把一不可证公式作为公理，其结果是系统不再具有一致性。但是命题演算不满足这样定义的完全性的要求：一公理系统是完全的，当且仅当对于任一公式A，或者A是可证的，或者乛A是可证的。例如，让A表示P∨q，则A和乛A在系统中都是不可证的。
命题演算中的任一公式都是可判定的。对于任一命题公式A，都有能行的方法，即每一步都是由某个事先给定的规则明确规定了的并且在有穷步骤内可以完成的方法，来判定它是否重言式，是否系统中的定理。能行的方法有两种， 一种是真值表的方法，一种是范式的方法。
元逻辑对谓词演算系统的研究取得下面的成果：谓词演算满足一致性的要求，即谓词演算系统自身是协调的、无矛盾的，谓词演算的一致性定理有两种表述方式：（一） 一阶谓词演算是在古典的意义下一致的，即不可能有一公式A, A和乛A都在系统中可证；（二） 一阶谓词演算是语法一致的，即有一公式A,A在系统中是不可证的。从一致性定理出发，可以引出两个有效性定理：（一） 对任一给定的整数K (K≥1)，一阶谓词的定理都是K普遍有效的；（二） 一阶谓词演算的定理都是普遍有效的。
一阶谓词演算满足完全性的要求，即对于任一公式A，或者A在系统中可证，或者乛A是可满足的。从完全性定理可以得出，如果A是协调的，则A是可满足的（有一模型）。但是一阶谓词演算不满足如下意义的两种完全性的要求：（一） 古典的完全性，对任一公式A，或者A可证，或者乛A可证；（二） 语法的完全性，把一不可证公式作为公理增加到已有的公理中，可以使这系统里任一公式都是可证的。
谓词演算中的公式一般地是不可判定的，即不存在一种能行的方法来判定任一谓词公式是否普遍有效，是否可证，是否可满足。这是因为谓词公式所涉及的个体域都是无穷的。但是，在判定问题一般地不能解决的情况下，某些特殊类型的公式的判定问题是可以解决的。
元逻辑通过对一般形式系统的研究也获得了许多元定理。其中两个最重要的元定理是哥德尔不完全性定理和塔斯基关于真语句的定义。
哥德尔不完全性定理由两个定理组成：（一） 一个包括初等数论的形式系统P，如果P是协调的，则P就是不完全的，即存在语句A,A是真的，但在系统中是不可证的。这被称为第一不完全性定理。（二）形式数论系统的协调性的证明不可能在形式数论系统中实现。这被称为第二不完全性定理。哥德尔不完全性定理表明希尔伯特的形式纲领无法实现，对整个数学的研究产生了巨大的影响。
塔斯基在研究形式语言时，得出两个重要的结论：（一） 对每一形式化语言的真语句的定义，必须借助于元语言来实现，元语言的层次要高于作为研究对象的语言层次；（二） 如果元语言的层次至多等于所研究的语言自身，这样的定义就不能成立。塔斯基由此建立了语言层次论，其基本思想是：必须分清对象语言和元语言，关于一语句的真、假的表达，必须用层次上高于这种语言的语言来表达。
在有了机械程序（算法）的精确概念后，元逻辑进一步研究了可判定问题，不仅能证明某些问题类是机械地可解的，而且能证明某些问题类是机械地不可解的，从而得到可判定性的明确概念。邱吉证明了人们感兴趣的大多数形式系统(对于任一语句是否定理，是否可证)是不可判定的。