His main results

• Using the theory of better quasi ordered sets, introduced by Nash-Williams, (an extension of the notion of well-quasi-ordering
  Well-quasi-ordering
  In mathematics, specifically order theory, a well-quasi-ordering or wqo is a well-founded quasi-ordering with an additional restriction on sequences - that there is no infinite sequence x_i with x_i \not \le x_j for all i...
  
  ), he proved Fraïssé's
  Roland Fraïssé
  Roland Fraïssé was a French mathematical logician. He received his doctoral degree from the University of Paris in 1953. In his thesis, Fraïssé used the back-and-forth method to determine whether two model-theoretic structures were elementarily equivalent...
  
   conjecture: if (A₀,≤),(A₁,≤),...,(A_i,≤),,, are countable ordered sets, then for some i<j (A_i,≤) isomorphically embeds into (A_j,≤). This also holds if the ordered sets are countable unions of scattered
  Scattered order
  In mathematics, specifically order theory, a scattered order is a linear order that contains no densely ordered subset with more than 1 element....
  
   ordered sets.
• He proved the consistency of the Borel conjecture, i.e., the statement that every strong measure zero set is countable. This important independence result was the first when a forcing, adding a real, was iterated with countable support iteration. This method was later used by Shelah
  Saharon Shelah
  Saharon Shelah is an Israeli mathematician. He is a professor of mathematics at the Hebrew University of Jerusalem and Rutgers University in New Jersey.-Biography:...
  
   to introduce proper and semiproper forcing.
• He proved the existence of a Laver function
  Laver function
  In set theory, a Laver function is a function connected with supercompact cardinals.-Definition:...
  
   for supercompact cardinals. With the help of this, he proved the following result. If κ is supercompact, there is a κ-c.c. forcing
  Forcing (mathematics)
  In the mathematical discipline of set theory, forcing is a technique invented by Paul Cohen for proving consistency and independence results. It was first used, in 1963, to prove the independence of the axiom of choice and the continuum hypothesis from Zermelo–Fraenkel set theory...
  
   notion (P, ≤) such that after forcing with (P, ≤) the following holds: κ is supercompact and remains supercompact in any forcing extension via a κ-directed closed forcing. This statement is used, for example in the proof of the consistency of the proper forcing axiom
  Proper Forcing Axiom
  In the mathematical field of set theory, the proper forcing axiom is a significant strengthening of Martin's axiom, where forcings with the countable chain condition are replaced by proper forcings.- Statement :...
  
   and variants.
• Laver and Shelah
  Saharon Shelah
  Saharon Shelah is an Israeli mathematician. He is a professor of mathematics at the Hebrew University of Jerusalem and Rutgers University in New Jersey.-Biography:...
  
   proved that it is consistent that the continuum hypothesis holds and there are no ℵ₂-Suslin tree
  Suslin tree
  In mathematics, a Suslin tree is a tree of height ω1 such thatevery branch and every antichain is at most countable. Every Suslin tree is an Aronszajn tree....
  
  s.
• Laver proved that the perfect subtree version of the Halpern–Läuchli theorem holds for the product of infinitely many trees. This solved a longstanding open question.
• Laver started investigating the algebra that j generates where j:V_λ→V_λ is some elementary embedding. This algebra is the free left-distributive algebra on one generator. For this he introduced Laver table
  Laver table
  In mathematics, Laver tables are tables of numbers that have certain properties.- Definition :...
  
  s.
• He also showed that if V[G] is a (set-)forcing
  Forcing (mathematics)
  In the mathematical discipline of set theory, forcing is a technique invented by Paul Cohen for proving consistency and independence results. It was first used, in 1963, to prove the independence of the axiom of choice and the continuum hypothesis from Zermelo–Fraenkel set theory...
  
   extension of V
  Von Neumann universe
  In set theory and related branches of mathematics, the von Neumann universe, or von Neumann hierarchy of sets, denoted V, is the class of hereditary well-founded sets...
  
  , then V is a class
  Class (set theory)
  In set theory and its applications throughout mathematics, a class is a collection of sets which can be unambiguously defined by a property that all its members share. The precise definition of "class" depends on foundational context...
  
  in V[G].